English
The product of the word obtained by smul with the empty word shows consistency with unit action: (w.prod φ) • empty = w.
Русский
Произведение полученного слова после умножения на пустое слово согласуется с единичным действием: (w.prod φ) • empty = w.
LaTeX
$$$(w.prod φ) \\cdot empty = w.$$$
Lean4
@[simp]
theorem prod_smul_empty (w : NormalWord d) : (w.prod φ) • empty = w := by
induction w using consRecOn with
| ofGroup => simp [ofGroup, ReducedWord.prod, of_smul_eq_smul, group_smul_def]
| cons g u w h1 h2
ih =>
rw [prod_cons, ← mul_assoc, mul_smul, ih, mul_smul, t_pow_smul_eq_unitsSMul, of_smul_eq_smul, unitsSMul]
rw [dif_neg (not_cancels_of_cons_hyp u w h2)]
-- Before https://github.com/leanprover/lean4/pull/2644, this was just
-- simp [unitsSMulGroup, (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1,
-- -SetLike.coe_sort_coe]
-- ext <;> simp [-SetLike.coe_sort_coe]
simp only [unitsSMulGroup, (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1, smul_cons]
ext <;> simp [-SetLike.coe_sort_coe]
rw [(d.compl _).equiv_snd_eq_inv_mul, (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1]
simp
