English
To prove a property for all Unitization R A it suffices to prove it for elements of the form inl r + a.
Русский
Чтобы доказать свойство для всех Unitization R A достаточно доказать его для элементов вида inl r + a.
LaTeX
$$$[AddZeroClass R] [AddZeroClass A]\\\\{P: Unitization R A \\\\to Prop\\\\} \\\\Leftarrow \\\\text{(inl_add_inr : ∀ r a, P (inl r + (a : Unitization R A)))} \\\\Rightarrow ∀ x, P x.$$$
Lean4
/-- To show a property hold on all `Unitization R A` it suffices to show it holds
on terms of the form `inl r + a`.
This can be used as `induction x`. -/
@[elab_as_elim, induction_eliminator, cases_eliminator]
theorem ind {R A} [AddZeroClass R] [AddZeroClass A] {P : Unitization R A → Prop}
(inl_add_inr : ∀ (r : R) (a : A), P (inl r + (a : Unitization R A))) (x) : P x :=
inl_fst_add_inr_snd_eq x ▸ inl_add_inr x.1 x.2
