English
There is an induction principle for units of the quotient c.Quotient: to prove a property p on every unit, it is enough to prove p for the unit arising from any pair x, y ∈ M with witnesses showing x*y and y*x lie in the congruence class of 1, and then assemble via the given H.
Русский
Существует принцип математной индукции по единицам карджа: чтобы доказать свойство p для любой единицы, достаточно доказать его для единицы, полученной из любых x, y ∈ M с доказательствами того, что x*y и y*x принадлежат классу 1 по конгруэнции, и далее использовать имеющееся условие.
LaTeX
$$$\text{induction_on_units} : \forall p:\nUnits(c.Quotient) \to Prop,\; u:\, Units(c.Quotient) \\to (\forall x\, y:\, M\, (hxy:\, c(x y)1) (hyx:\, c( y x)1), p \langle x, y, c.eq.2 hxy, c.eq.2 hyx\rangle) \Rightarrow p u$$$
Lean4
@[to_additive (attr := elab_as_elim)]
theorem induction_on_units {p : Units c.Quotient → Prop} (u : Units c.Quotient)
(H : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p ⟨x, y, c.eq.2 hxy, c.eq.2 hyx⟩) : p u :=
by
rcases u with ⟨⟨x⟩, ⟨y⟩, h₁, h₂⟩
exact H x y (c.eq.1 h₁) (c.eq.1 h₂)
