English
An induction principle on FreeMonoid with cases for 1 and of x * a, providing a simple left-to-right induction over words.
Русский
Принцип индукции по FreeMonoid с базовым случаем 1 и переходом через of x * a.
LaTeX
$$$\\\\forall p: FreeMonoid α \\to Prop, \\\\; p(1) \\to (\\\\forall x, p(x) \\to p(of x * a)) \\to p(a)$$$
Lean4
/-- An induction principle on free monoids, with cases for `1`, `FreeMonoid.of` and `*`. -/
@[to_additive (attr := elab_as_elim, induction_eliminator) /--
An induction principle on free monoids, with cases for `0`, `FreeAddMonoid.of` and `+`. -/
]
protected theorem inductionOn {C : FreeMonoid α → Prop} (z : FreeMonoid α) (one : C 1)
(of : ∀ (x : α), C (FreeMonoid.of x)) (mul : ∀ (x y : FreeMonoid α), C x → C y → C (x * y)) : C z :=
List.rec one (fun _ _ ih => mul [_] _ (of _) ih) z
