English
In the free product construction, the product of a suitably constructed inverse word with the original word collapses to the identity, reflecting inverse cancellation.
Русский
В конструировании свободного произведения произведение правильно построенного слова-обратного с оригинальным словом сводится к тождественному элементу, отражая удаление пары "обратных".
LaTeX
$$$ coprodCon(G,H)\Big(\mathrm{ofList}(x.toList.map(\mathrm{Sum.mapInvInv}).reverse) \cdot x\Big) = 1, \; x \in FreeMonoid(G \oplus H). $$$
Lean4
@[to_additive]
theorem con_inv_mul_cancel (x : FreeMonoid (G ⊕ H)) :
coprodCon G H (ofList (x.toList.map (Sum.map Inv.inv Inv.inv)).reverse * x) 1 :=
by
rw [← mk_eq_mk, map_mul, map_one]
induction x using FreeMonoid.inductionOn' with
| one => simp
| mul_of x xs
ihx =>
simp only [toList_of_mul, map_cons, reverse_cons, ofList_append, map_mul, ofList_singleton]
rwa [mul_assoc, ← mul_assoc (mk (of _)), mk_of_inv_mul, one_mul]
