-- Mathlib/GroupTheory/Coxeter/Basic.lean
lemma getElem_alternatingWord (i j : B) (p k : ℕ) (hk : k < p) :
    (alternatingWord i j p)[k]'(by simp [hk]) = (if Even (p + k) then i else j)

Proof state:
case zero
B : Type u_1
i j : B
⊢ ∀ (k : ℕ) (hk : k < 0), (alternatingWord i j 0)[k] = if Even (0 + k) then i else j

Tactic:
intro k hk

Result:
case zero
B : Type u_1
i j : B
k : ℕ
hk : k < 0
⊢ (alternatingWord i j 0)[k] = if Even (0 + k) then i else j

Proof state:
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k✝ k : ℕ
hk✝ : k + 1 < n + 1
hk : k < n
m : ℕ
⊢ m ≤ 2 + m

Tactic:
omega

Result:
no goals

Proof state:
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k✝ k : ℕ
hk✝ : k + 1 < n + 1
hk : k < n
⊢ (if Even (n + k) then i else j) = if Even (2 + n + k) then i else j

Tactic:
have even_add_two (m : ℕ) : Even (2 + m) ↔ Even m := by
  simp only [add_tsub_cancel_right, even_two, (Nat.even_sub (by omega : m ≤ 2 + m)).mp]

Result:
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k✝ k : ℕ
hk✝ : k + 1 < n + 1
hk : k < n
even_add_two : ∀ (m : ℕ), Even (2 + m) ↔ Even m
⊢ (if Even (n + k) then i else j) = if Even (2 + n + k) then i else j

Proof state:
case pos
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k✝ k : ℕ
hk✝ : k + 1 < n + 1
hk : k < n
even_add_two : ∀ (m : ℕ), Even (2 + m) ↔ Even m
h_even : Even (n + k)
⊢ i = if Even (2 + n + k) then i else j

Tactic:
rw [← even_add_two (n+k), ← Nat.add_assoc 2 n k] at h_even

Result:
case pos
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k✝ k : ℕ
hk✝ : k + 1 < n + 1
hk : k < n
even_add_two : ∀ (m : ℕ), Even (2 + m) ↔ Even m
h_even : Even (2 + n + k)
⊢ i = if Even (2 + n + k) then i else j

Proof state:
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k✝ k : ℕ
hk : k + 1 < n + 1
⊢ ((if Even n then j else i) :: alternatingWord i j n)[k + 1] = if Even (n + 1 + (k + 1)) then i else j

Tactic:
simp only [add_lt_add_iff_right] at hk h

Result:
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k✝ k : ℕ
hk✝ : k + 1 < n + 1
hk : k < n
⊢ ((if Even n then j else i) :: alternatingWord i j n)[k + 1] = if Even (n + 1 + (k + 1)) then i else j

Proof state:
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k✝ k : ℕ
hk✝ : k + 1 < n + 1
hk : k < n
⊢ ((if Even n then j else i) :: alternatingWord i j n)[k + 1] = if Even (n + 1 + (k + 1)) then i else j

Tactic:
simp only [getElem_cons_succ, h k hk]

Result:
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k✝ k : ℕ
hk✝ : k + 1 < n + 1
hk : k < n
⊢ (if Even (n + k) then i else j) = if Even (n + 1 + (k + 1)) then i else j

Proof state:
case neg
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k✝ k : ℕ
hk✝ : k + 1 < n + 1
hk : k < n
even_add_two : ∀ (m : ℕ), Even (2 + m) ↔ Even m
h_even : ¬Even (n + k)
⊢ j = if Even (2 + n + k) then i else j

Tactic:
rw [← even_add_two (n+k), ← Nat.add_assoc 2 n k] at h_even

Result:
case neg
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k✝ k : ℕ
hk✝ : k + 1 < n + 1
hk : k < n
even_add_two : ∀ (m : ℕ), Even (2 + m) ↔ Even m
h_even : ¬Even (2 + n + k)
⊢ j = if Even (2 + n + k) then i else j

Proof state:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝¹ : Group W
inst✝ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
hk : k < p
⊢ k < (alternatingWord i j p).length

Tactic:
simp [hk]

Result:
no goals

Proof state:
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k✝ k : ℕ
hk✝ : k + 1 < n + 1
hk : k < n
m : ℕ
⊢ Even (2 + m) ↔ Even m

Tactic:
simp only [add_tsub_cancel_right, even_two, (Nat.even_sub (by omega : m ≤ 2 + m)).mp]

Result:
no goals

Proof state:
B : Type u_1
i j : B
p k : ℕ
hk : k < p
⊢ (alternatingWord i j p)[k] = if Even (p + k) then i else j

Tactic:
revert k

Result:
B : Type u_1
i j : B
p : ℕ
⊢ ∀ (k : ℕ) (hk : k < p), (alternatingWord i j p)[k] = if Even (p + k) then i else j

Proof state:
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k : ℕ
hk : 0 < n + 1
⊢ ((if Even n then j else i) :: alternatingWord i j n)[0] = if Even (n + 1 + 0) then i else j

Tactic:
by_cases h2 : Even n

Result:
case pos
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k : ℕ
hk : 0 < n + 1
h2 : Even n
⊢ ((if Even n then j else i) :: alternatingWord i j n)[0] = if Even (n + 1 + 0) then i else j

case neg
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k : ℕ
hk : 0 < n + 1
h2 : ¬Even n
⊢ ((if Even n then j else i) :: alternatingWord i j n)[0] = if Even (n + 1 + 0) then i else j

Proof state:
case pos
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k✝ k : ℕ
hk✝ : k + 1 < n + 1
hk : k < n
even_add_two : ∀ (m : ℕ), Even (2 + m) ↔ Even m
h_even : Even (n + k)
⊢ (if Even (n + k) then i else j) = if Even (2 + n + k) then i else j

Tactic:
rw [if_pos h_even]

Result:
case pos
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k✝ k : ℕ
hk✝ : k + 1 < n + 1
hk : k < n
even_add_two : ∀ (m : ℕ), Even (2 + m) ↔ Even m
h_even : Even (n + k)
⊢ i = if Even (2 + n + k) then i else j

Proof state:
case succ
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k : ℕ
hk : k < n + 1
⊢ (alternatingWord i j (n + 1))[k] = if Even (n + 1 + k) then i else j

Tactic:
simp_rw [alternatingWord_succ' i j n]

Result:
case succ
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k : ℕ
hk : k < n + 1
⊢ ((if Even n then j else i) :: alternatingWord i j n)[k] = if Even (n + 1 + k) then i else j

Proof state:
case pos
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k : ℕ
hk : 0 < n + 1
h2 : Even n
⊢ ((if Even n then j else i) :: alternatingWord i j n)[0] = if Even (n + 1 + 0) then i else j

Tactic:
simp only [h2, ↓reduceIte, getElem_cons_zero, add_zero,
  (by simp [Even.add_one, h2] : ¬Even (n + 1))]

Result:
no goals

Proof state:
case pos
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k✝ k : ℕ
hk✝ : k + 1 < n + 1
hk : k < n
even_add_two : ∀ (m : ℕ), Even (2 + m) ↔ Even m
h_even : Even (2 + n + k)
⊢ i = if Even (2 + n + k) then i else j

Tactic:
rw [if_pos h_even]

Result:
no goals

Proof state:
case neg
B : Type u_1
i j : B
n : ℕ
h : ∀ (k : ℕ) (hk : k < n), (alternatingWord i j n)[k] = if Even (n + k) then i else j
k : ℕ
hk : 0 < n + 1
h2 : ¬Even n
⊢ ((if Even n then j else i) :: alternatingWord i j n)[0] = if Even (n + 1 + 0) then i else j

Tactic:
simp only [h2, ↓reduceIte, getElem_cons_zero, add_zero,
  Odd.add_one (Nat.not_even_iff_odd.mp h2)]

Result:
no goals