English
For any property P on CoprodI M, if P holds for the unit 1 and is preserved when multiplied on the left by an element from any factor M_i, then P holds for every element of CoprodI M.
Русский
Для любого свойства P над CoprodI M, если P выполняется на единице 1 и если из P модуляется при умножении слева на элемент из любого M_i, то P выполняется для каждого элемента CoprodI M.
LaTeX
$$$\forall \text{motive},\; (\forall i\, m\in M_i)\; \big( P(1) \big) \land \big( \forall m\, x, P(x) \to P(\mathrm{of}\, m * x) \big) \Rightarrow P(m)$$$
Lean4
@[elab_as_elim]
theorem induction_left {motive : CoprodI M → Prop} (m : CoprodI M) (one : motive 1)
(mul : ∀ {i} (m : M i) x, motive x → motive (of m * x)) : motive m := by
induction m using Submonoid.induction_of_closure_eq_top_left mclosure_iUnion_range_of with
| one => exact one
| mul_left x hx y ihy =>
obtain ⟨i, m, rfl⟩ : ∃ (i : ι) (m : M i), of m = x := by simpa using hx
exact mul m y ihy
