English
The consRecOn construction has corresponding proof obligations showing consistency with the recursive definition of NormalWord.
Русский
У конструктора consRecOn есть доказательства, обеспечивающие консистентность с рекурсивным определением NormalWord.
LaTeX
$$$$\text{consRecOn}_{proof} $$$$
Lean4
@[simp]
theorem prod_summand_smul {i : ι} (g : G i) (w : NormalWord d) : (g • w).prod = of i g * w.prod := by
simp only [prod, summand_smul_def', equivPair, rcons, Word.equivPair_symm, Equiv.coe_fn_mk, Equiv.coe_fn_symm_mk,
Word.equivPair_smul_same, Word.equivPair_tail_eq_inv_smul, Word.rcons_eq_smul, ← of_apply_eq_base φ i,
MonoidHom.apply_ofInjective_symm, equiv_fst_eq_mul_inv, mul_assoc, map_mul, map_inv, Word.prod_smul, ofCoprodI_of,
inv_mul_cancel_left, mul_inv_cancel_left]
