English
There is an induction principle for elements of CoprodI M, stating that to prove a property for all elements it suffices to prove it for the identity and to show it is preserved under the basic coproduct operations (of and mul).
Русский
Существует принципы индукции для элементов CoprodI M: для доказательства свойства для всех элементов достаточно доказать его для единицы и показать, что оно сохраняется при операциях включения (of) и умножения (mul).
LaTeX
$$$ \\forall m : \\mathrm{CoprodI} M,\\; \\text{motive}(m) $ движется по индукции через конструкторы 'one' и 'of'/'mul'.$$
Lean4
@[elab_as_elim]
theorem induction_on {motive : CoprodI M → Prop} (m : CoprodI M) (one : motive 1) (of : ∀ (i) (m : M i), motive (of m))
(mul : ∀ x y, motive x → motive y → motive (x * y)) : motive m := by
induction m using CoprodI.induction_left with
| one => exact one
| mul m x hx => exact mul _ _ (of _ _) hx
