English
In the alternating word construction, the (k+1)-st element of the leftInvSeq of alternation is conjugate by s_i of the k-th element of the opposite alternating word.
Русский
В построении чередующегося слова (alternatingWord) (k+1)-й элемент левойInvSeq является сопряжением по s_i к k-му элементу противоположного чередующегося слова.
LaTeX
$$$(\mathrm{lis}(\text{alternatingWord } i j (2p)))_{k+1} = \mathrm{MulAut.conj}(s_i)\Bigl((\mathrm{lis}(\text{alternatingWord } j i (2p)))_{k}\Bigr)$$$
Lean4
theorem getElem_succ_leftInvSeq_alternatingWord (i j : B) (p k : ℕ) (h : k + 1 < 2 * p) :
(lis(alternatingWord i j (2 * p)))[k + 1]'(by simpa using h) =
MulAut.conj (s i) ((lis(alternatingWord j i (2 * p)))[k]'(by simp; cutsat)) :=
by
rw [cs.getElem_leftInvSeq (alternatingWord i j (2 * p)) (k + 1) (by simp [h]),
cs.getElem_leftInvSeq (alternatingWord j i (2 * p)) k (by simp; cutsat)]
simp only [MulAut.conj, listTake_succ_alternatingWord i j p k h, cs.wordProd_cons, mul_assoc, mul_inv_rev, inv_simple,
MonoidHom.coe_mk, OneHom.coe_mk, MulEquiv.coe_mk, Equiv.coe_fn_mk, mul_right_inj, mul_left_inj]
rw [getElem_alternatingWord_swapIndices i j (2 * p) k]
cutsat
