English
To prove a property holds for all elements of TrivSqZeroExt R M it suffices to prove it for elements of the form inl r + inr m.
Русский
Доказательство свойства для всех элементов TrivSqZeroExt R M сводится к доказательству его для элементов вида inl r + inr m.
LaTeX
$$$\forall P: \mathrm{TrivSqZeroExt}~R~M \to \text{Prop},\ (\forall r\, m, P(\mathrm{inl}(r) + \mathrm{inr}(m))) \Rightarrow \forall x, P(x)$$$
Lean4
/-- To show a property hold on all `TrivSqZeroExt R M` it suffices to show it holds
on terms of the form `inl r + inr m`. -/
@[elab_as_elim, induction_eliminator, cases_eliminator]
theorem ind {R M} [AddZeroClass R] [AddZeroClass M] {P : TrivSqZeroExt R M → Prop}
(inl_add_inr : ∀ r m, P (inl r + inr m)) (x) : P x :=
inl_fst_add_inr_snd_eq x ▸ inl_add_inr x.1 x.2
