-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem getElem_leftInvSeq_alternatingWord
    (i j : B) (p k : ℕ) (h : k < 2 * p) :
    (lis (alternatingWord i j (2 * p)))[k]'(by simp; omega) =
    π alternatingWord j i (2 * k + 1)

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

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 < 2 * p
⊢ (cs.leftInvSeq (alternatingWord i j (2 * p)))[k] = cs.wordProd (alternatingWord j i (2 * k + 1))

Tactic:
induction k generalizing i j with
| zero =>
  simp only [CoxeterSystem.getElem_leftInvSeq cs (alternatingWord i j (2 * p)) 0 (by simp [h]),
    take_zero, wordProd_nil, one_mul, inv_one, mul_one, alternatingWord, concat_eq_append,
    nil_append, wordProd_singleton]
  apply congr_arg
  simp only [getElem_alternatingWord i j (2 * p) 0 (by simp [h]), add_zero, even_two,
    Even.mul_right, ↓reduceIte]
| succ k hk =>
  simp only [getElem_succ_leftInvSeq_alternatingWord cs i j p k h, hk _ _ (by omega),
    MulAut.conj_apply, inv_simple, alternatingWord_succ' j i, even_two, Even.mul_right,
    ↓reduceIte, wordProd_cons]
  rw [(by ring: 2 * (k + 1) = 2 * k + 1 + 1), alternatingWord_succ j i, wordProd_concat]
  simp [mul_assoc]

Result:
no goals

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

Tactic:
apply congr_arg

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

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 < 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 < 2 * p
⊢ k < (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 < 2 * p
⊢ k < 2 * p

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

Tactic:
simp only [getElem_alternatingWord i j (2 * p) 0 (by simp [h]), add_zero, even_two,
  Even.mul_right, ↓reduceIte]

Result:
no goals

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

Tactic:
simp only [CoxeterSystem.getElem_leftInvSeq cs (alternatingWord i j (2 * p)) 0 (by simp [h]),
  take_zero, wordProd_nil, one_mul, inv_one, mul_one, alternatingWord, concat_eq_append,
  nil_append, wordProd_singleton]

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

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

Tactic:
ring

Result:
no goals

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

Tactic:
rw [(by ring: 2 * (k + 1) = 2 * k + 1 + 1), alternatingWord_succ j i, wordProd_concat]

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

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

Tactic:
simp [mul_assoc]

Result:
no goals

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

Tactic:
omega

Result:
no goals

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

Tactic:
simp only [getElem_succ_leftInvSeq_alternatingWord cs i j p k h, hk _ _ (by omega),
  MulAut.conj_apply, inv_simple, alternatingWord_succ' j i, even_two, Even.mul_right,
  ↓reduceIte, wordProd_cons]

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

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

Tactic:
simp [h]

Result:
no goals