English
If the head of a NeWord equals its last letter, then lifting preserves nontriviality; more concretely, for w : NeWord H i i with i ≠ k, lift f w.prod ≠ 1.
Русский
Если голова NeWord совпадает с последней буквой, то образ lift сохраняет нетривиальность; например, для w : NeWord H i i выполняется lift f w.prod ≠ 1.
LaTeX
$$$$\\text{lift}(f)\\, w.\\text{prod} \\neq 1 \\quad\\text{when } w:\\ NeWord\\ H\\ i\\ i.$$$
Lean4
theorem lift_word_prod_nontrivial_of_head_card {i j} (w : NeWord H i j) (hcard : 3 ≤ #(H i)) (hheadtail : i ≠ j) :
lift f w.prod ≠ 1 := by
obtain ⟨h, hn1, hnh⟩ := Cardinal.three_le hcard 1 w.head⁻¹
have hnot1 : h * w.head ≠ 1 := by
rw [← div_inv_eq_mul]
exact div_ne_one_of_ne hnh
let w' : NeWord H i i :=
NeWord.append (NeWord.mulHead w h hnot1) hheadtail.symm (NeWord.singleton h⁻¹ (inv_ne_one.mpr hn1))
have hw' : lift f w'.prod ≠ 1 := lift_word_prod_nontrivial_of_head_eq_last f X hXnonempty hXdisj hpp w'
intro heq1
apply hw'
simp [w', heq1]
