English
An induction principle for elements of the coproduct M ∗ N: if a property C holds for 1, is preserved when multiplying on the left by inl-multiples and inr-multiples, then C holds for all elements.
Русский
Принцип индукции по элементам копродукта M ∗ N: если свойство C выполняется для 1, сохраняется под умножением слева на изображения inl и inr, то C верно для всех элементов.
LaTeX
$$$\forall C:(M\ast N)\to\mathrm{Prop},\; C(1) \land \left(\forall m, x, C(x) \to C(inl(m) * x)\right) \land \left(\forall n, x, C(x) \to C(inr(n) * x)\right) \Rightarrow \forall m, C(m).$$$
Lean4
@[to_additive (attr := elab_as_elim)]
theorem induction_on' {C : M ∗ N → Prop} (m : M ∗ N) (one : C 1) (inl_mul : ∀ m x, C x → C (inl m * x))
(inr_mul : ∀ n x, C x → C (inr n * x)) : C m :=
by
rcases mk_surjective m with ⟨x, rfl⟩
induction x using FreeMonoid.inductionOn' with
| one => exact one
| mul_of x xs ih =>
cases x with
| inl m => simpa using inl_mul m _ ih
| inr n => simpa using inr_mul n _ ih
