English
The Word data type in CoprodI encodes finite words made from pairs (i, m) with i a index and m ∈ M_i; there are constructors for empty words and concatenation of words, and a head-tail decomposition describing the word’s first component and rest.
Русский
Тип Word в CoprodI кодирует конечные слова, состоящие из пар (i, m) с индексом i и элементом m ∈ M_i; есть конструкторы пустого слова и конкатенации, а также разложение на голову и хвост.
LaTeX
$$$\\mathrm{Word} = \\text{finite sequences of }(i,m)\\text{ with head-tail structure.}$$$
Lean4
/-- See note [partially-applied ext lemmas]. -/
@[ext 1100] -- This needs a higher `ext` priority
theorem ext_hom (f g : CoprodI M →* N) (h : ∀ i, f.comp (of : M i →* _) = g.comp of) : f = g :=
(MonoidHom.cancel_right Con.mk'_surjective).mp <|
FreeMonoid.hom_eq fun ⟨i, x⟩ =>
by
rw [MonoidHom.comp_apply, MonoidHom.comp_apply, ← of_apply]
unfold CoprodI
rw [← MonoidHom.comp_apply, ← MonoidHom.comp_apply, h]
