English
The reduced word product respects smul by a word: applying a word g to w corresponds to multiplying the image by g on the left in the extension.
Русский
Редуцированное произведение слова учитывает умножение: применение слова g к w соответствует левой умножению на g в расширении.
LaTeX
$$$\\mathrm{ReducedWord}.prod(φ, (w)^{\\ast}) = g \\cdot (w^{\\mathrm{prod}}).$$$
Lean4
theorem prod_unitsSMul (u : ℤˣ) (w : NormalWord d) :
(unitsSMul φ u w).prod φ = (t ^ (u : ℤ) * w.prod φ : HNNExtension G A B φ) :=
by
rw [unitsSMul]
split_ifs with hcan
· cases w using consRecOn
· simp [Cancels] at hcan
· cases hcan.2
simp only [unitsSMulWithCancel, id_eq, consRecOn_cons, prod_group_smul, prod_cons, zpow_neg]
rcases Int.units_eq_one_or u with (rfl | rfl)
· simp [equiv_eq_conj, mul_assoc]
· -- Before https://github.com/leanprover/lean4/pull/2644, this proof was just
-- simp [equiv_symm_eq_conj, mul_assoc].
simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, Units.val_neg, Units.val_one, Int.reduceNeg, zpow_neg,
zpow_one, inv_inv]
erw [equiv_symm_eq_conj]
simp [mul_assoc]
· simp only [unitsSMulGroup, SetLike.coe_sort_coe, prod_cons, prod_group_smul, map_mul, map_inv]
rcases Int.units_eq_one_or u with (rfl | rfl)
· -- Before https://github.com/leanprover/lean4/pull/2644, this proof was just
-- simp [equiv_eq_conj, mul_assoc, (d.compl _).equiv_snd_eq_inv_mul].
simp only [toSubgroup_neg_one, toSubgroup_one, toSubgroupEquiv_one, equiv_eq_conj, mul_assoc, Units.val_one,
zpow_one, inv_mul_cancel_left, mul_right_inj]
erw [(d.compl 1).equiv_snd_eq_inv_mul]
simp [mul_assoc]
· -- Before https://github.com/leanprover/lean4/pull/2644, this proof was just
-- simp [equiv_symm_eq_conj, mul_assoc, (d.compl _).equiv_snd_eq_inv_mul]
simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, Units.val_neg, Units.val_one, Int.reduceNeg, zpow_neg,
zpow_one, mul_assoc]
erw [equiv_symm_eq_conj, (d.compl (-1)).equiv_snd_eq_inv_mul]
simp [mul_assoc]
