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

Tactic:
by_cases h_even : Even (n + k)

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)
⊢ (if Even (n + k) then i else j) = if Even (2 + n + k) 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✝ 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

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
h2 : Even n
⊢ ¬Even (n + 1)

Tactic:
simp [Even.add_one, h2]

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✝ 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_neg 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 (n + k)
⊢ j = if Even (2 + n + k) 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 (2 + n + k)
⊢ j = if Even (2 + n + k) then i else j

Tactic:
rw [if_neg h_even]

Result:
no goals

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:
intro k hk

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
⊢ (alternatingWord i j (n + 1))[k] = if Even (n + 1 + 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
⊢ (if Even (n + k) then i else j) = if Even (n + 1 + (k + 1)) then i else j

Tactic:
ring_nf

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 (2 + n + 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:
simp only [not_lt_zero'] at hk

Result:
no goals