English
Extensionality for NonUnitalNonAssocSemiring: two instances are equal if their Add and Mul parts are equal.
Русский
Экстенсиональность для NonUnitalNonAssocSemiring: два экземпляра равны, если их части сложения и умножения совпадают.
LaTeX
$$$ \text{ext } (h\_add) (h\_mul) \Rightarrow inst = inst' $$$
Lean4
@[ext]
theorem ext ⦃inst₁ inst₂ : NonUnitalNonAssocSemiring R⦄ (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
(h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : inst₁ = inst₂ := by
-- Split into `AddMonoid` instance, `mul` function and properties.
rcases inst₁ with @⟨_, ⟨⟩⟩
rcases inst₂ with
@⟨_, ⟨⟩⟩
-- Prove equality of parts using already-proved extensionality lemmas.
congr; ext : 1; assumption
