-- Mathlib/GroupTheory/Coxeter/Inversion.lean
lemma getElem_succ_leftInvSeq_alternatingWord
    (i j : B) (p k : ℕ) (h : k + 1 < 2 * p) :
    (lis (alternatingWord i j (2 * p)))[k + 1]'(by simp; exact h) =
    MulAut.conj (s i) ((lis (alternatingWord j i (2 * p)))[k]'(by simp; omega))

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k < (alternatingWord j i (2 * p)).length

Tactic:
simp[h]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k < 2 * p

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k + 1 < (alternatingWord i j (2 * p)).length

Tactic:
simp[h]

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k < 2 * p

Tactic:
omega

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k < (cs.leftInvSeq (alternatingWord j i (2 * p))).length

Tactic:
simp

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k < 2 * p

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k + 1 < (cs.leftInvSeq (alternatingWord i j (2 * p))).length

Tactic:
simp

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k + 1 < 2 * p

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k + 1 < 2 * p

Tactic:
omega

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ cs.wordProd (take (k + 1) (alternatingWord i j (2 * p))) * cs.simple (alternatingWord i j (2 * p))[k + 1] *
      (cs.wordProd (take (k + 1) (alternatingWord i j (2 * p))))⁻¹ =
    (MulAut.conj (cs.simple i))
      (cs.wordProd (take k (alternatingWord j i (2 * p))) * cs.simple (alternatingWord j i (2 * p))[k] *
        (cs.wordProd (take k (alternatingWord j i (2 * p))))⁻¹)

Tactic:
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]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ cs.simple (alternatingWord i j (2 * p))[k + 1] = cs.simple (alternatingWord j i (2 * p))[k]

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ (cs.leftInvSeq (alternatingWord i j (2 * p)))[k + 1] =
    (MulAut.conj (cs.simple i)) (cs.leftInvSeq (alternatingWord j i (2 * p)))[k]

Tactic:
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[h]; omega)]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ cs.wordProd (take (k + 1) (alternatingWord i j (2 * p))) * cs.simple (alternatingWord i j (2 * p))[k + 1] *
      (cs.wordProd (take (k + 1) (alternatingWord i j (2 * p))))⁻¹ =
    (MulAut.conj (cs.simple i))
      (cs.wordProd (take k (alternatingWord j i (2 * p))) * cs.simple (alternatingWord j i (2 * p))[k] *
        (cs.wordProd (take k (alternatingWord j i (2 * p))))⁻¹)

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ cs.simple (alternatingWord i j (2 * p))[k + 1] = cs.simple (alternatingWord j i (2 * p))[k]

Tactic:
rw [getElem_alternatingWord_swapIndices i j (2 * p) k]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k + 1 < 2 * p

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k + 1 < 2 * p

Tactic:
exact h

Result:
no goals