English
If P(1) holds and for any x ∈ s, P(y) implies P(x·y) for all y in closure(s), then P holds for all elements of closure(s).
Русский
Если P(1) выполняется и для любого x ∈ s, P(y) ⇒ P(x·y) для всех y ∈ closure(s), тогда P выполняется для всех элементов closure(s).
LaTeX
$$$\\text{If }(\\text{one}: P(1)\\text{ and } (\\forall x\\in s)(\\forall y \\in closure(s)) (P(y) \\to P(x \\cdot y)) )\\ \\to\\ \\forall x \\in closure(s),\\ P(x).$$$
Lean4
@[to_additive (attr := elab_as_elim)]
theorem closure_induction_left {s : Set M} {motive : (m : M) → m ∈ closure s → Prop} (one : motive 1 (one_mem _))
(mul_left : ∀ x (hx : x ∈ s), ∀ y hy, motive y hy → motive (x * y) (mul_mem (subset_closure hx) hy)) {x : M}
(h : x ∈ closure s) : motive x h := by
simp_rw [closure_eq_mrange] at h
obtain ⟨l, rfl⟩ := h
induction l using FreeMonoid.inductionOn' with
| one => exact one
| mul_of x y ih =>
simp only [map_mul, FreeMonoid.lift_eval_of]
refine mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_)
simp only [closure_eq_mrange, mem_mrange, exists_apply_eq_apply]
