English
There is an induction principle for properties of elements with respect to the DirectSum decomposition: to prove a property for all elements of M, it suffices to prove it for zero, for homogeneous components, and that the property is preserved under addition.
Русский
Существует принцип индукции по декомпозиции: чтобы доказать свойство для всех элементов M, достаточно доказать его для нуля, для однородных компонентов и что свойство сохраняется при сложении.
LaTeX
$$$\forall m \in M, P(m)$ follows from $P(0)$, $P$ on each component, and $P(m), P(n) \Rightarrow P(m+n)$.$$
Lean4
@[elab_as_elim]
protected theorem inductionOn {motive : M → Prop} (zero : motive 0) (homogeneous : ∀ {i} (m : ℳ i), motive (m : M))
(add : ∀ m m' : M, motive m → motive m' → motive (m + m')) : ∀ m, motive m :=
by
let ℳ' : ι → AddSubmonoid M := fun i ↦
(⟨⟨ℳ i, fun x y ↦ AddMemClass.add_mem x y⟩, (ZeroMemClass.zero_mem _)⟩ : AddSubmonoid M)
haveI t : DirectSum.Decomposition ℳ' :=
{ decompose' := DirectSum.decompose ℳ
left_inv := fun _ ↦ (decompose ℳ).left_inv _
right_inv := fun _ ↦ (decompose ℳ).right_inv _ }
have mem : ∀ m, m ∈ iSup ℳ' := fun _m ↦
(DirectSum.IsInternal.addSubmonoid_iSup_eq_top ℳ' (Decomposition.isInternal ℳ')).symm ▸ trivial
exact fun m ↦ @AddSubmonoid.iSup_induction _ _ _ ℳ' _ _ (mem m) (fun i m h ↦ homogeneous ⟨m, h⟩) zero add
