English
Let w1 and w2 be two normals words in d. For a fixed i, if the left-multiplication by φ i w1.head on w1 equals the left-multiplication by φ i w2.head on w2 after transporting through CoprodI.of, then w1 and w2 are equal.
Русский
Пусть w1 и w2 — нормальные слова в d. При фиксированном i если левая умножение на φ i w1.head действует на w1 так же, как левая умножение на φ i w2.head на w2 после переноса через CoprodI.of, тогда w1 = w2.
LaTeX
$$$$\\forall w_1,w_2 \\in \\mathrm{NormalWord}\, d, \\forall i,\\; \\mathrm{CoprodI.of}(\\phi i\\, w_1.head) \\cdot w_1.toWord = \\mathrm{CoprodI.of}(\\phi i\\, w_2.head) \\cdot w_2.toWord \\Rightarrow w_1 = w_2.$$$$
Lean4
theorem ext_smul {w₁ w₂ : NormalWord d} (i : ι)
(h : CoprodI.of (φ i w₁.head) • w₁.toWord = CoprodI.of (φ i w₂.head) • w₂.toWord) : w₁ = w₂ :=
by
rcases w₁ with ⟨w₁, h₁, hw₁⟩
rcases w₂ with ⟨w₂, h₂, hw₂⟩
dsimp at *
rw [smul_eq_iff_eq_inv_smul, ← mul_smul] at h
subst h
simp only [← map_inv, ← map_mul] at hw₁
have : h₁⁻¹ * h₂ = 1 := eq_one_of_smul_normalized w₂ (h₁⁻¹ * h₂) hw₂ hw₁
rw [inv_mul_eq_one] at this; subst this
simp
