English
If two MulOneClass structures on the same carrier have identical multiplication, then the two structures are equal.
Русский
Если на одной носители задано два объекта MulOneClass с одинаковой операцией умножения, то эти структуры равны.
LaTeX
$$$\\forall M\\, \\forall m_1,m_2:\\text{MulOneClass } M,\\; m_1.mul = m_2.mul \\Rightarrow m_1 = m_2.$$$
Lean4
@[to_additive (attr := ext)]
theorem ext {M : Type u} : ∀ ⦃m₁ m₂ : MulOneClass M⦄, m₁.mul = m₂.mul → m₁ = m₂ :=
by
rintro @⟨@⟨⟨one₁⟩, ⟨mul₁⟩⟩, one_mul₁, mul_one₁⟩ @⟨@⟨⟨one₂⟩, ⟨mul₂⟩⟩, one_mul₂, mul_one₂⟩
⟨rfl⟩
-- FIXME (See https://github.com/leanprover/lean4/issues/1711)
-- congr
suffices one₁ = one₂ by cases this; rfl
exact (one_mul₂ one₁).symm.trans (mul_one₁ one₂)
