-- Mathlib/GroupTheory/Coxeter/Basic.lean
lemma listTake_alternatingWord (i j : B) (p k : ℕ) (h : k < 2 * p) :
    List.take k (alternatingWord i j (2 * p)) =
    if Even k then alternatingWord i j k else alternatingWord j i k

Proof state:
case neg
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
hk : take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h_even : ¬Even k
⊢ take (k + 1) (alternatingWord i j (2 * p)) =
    if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)

Tactic:
simp only [h_even, ↓reduceIte] at hk

Result:
case neg
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ take (k + 1) (alternatingWord i j (2 * p)) =
    if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)

Proof state:
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ k < (alternatingWord i j (2 * p)).length

Tactic:
simp [h]

Result:
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ k < 2 * p

Proof state:
case pos
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
hk : take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h_even : Even k
⊢ take (k + 1) (alternatingWord i j (2 * p)) =
    if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)

Tactic:
simp only [h_even, ↓reduceIte] at hk

Result:
case pos
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ take (k + 1) (alternatingWord i j (2 * p)) =
    if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)

Proof state:
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ k < (alternatingWord i j (2 * p)).length

Tactic:
simp [h]

Result:
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ k < 2 * p

Proof state:
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
⊢ k < 2 * p

Tactic:
omega

Result:
no goals

Proof state:
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ Odd (2 * p + k)

Tactic:
apply Nat.odd_add.mpr

Result:
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ Odd (2 * p) ↔ Even k

Proof state:
case pos.h
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ (alternatingWord i j (2 * p))[k] = i

Tactic:
rw [getElem_alternatingWord i j (2*p) k (by omega)]

Result:
case pos.h
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ (if Even (2 * p + k) then i else j) = i

Proof state:
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ Even (2 * p + k)

Tactic:
apply Nat.even_add.mpr

Result:
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ Even (2 * p) ↔ Even k

Proof state:
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ Even (k + 1)

Tactic:
simp at h_even

Result:
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
h_even : Odd k
⊢ Even (k + 1)

Proof state:
case pos
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ (take k (alternatingWord i j (2 * p))).concat (alternatingWord i j (2 * p))[k] =
    (take k (alternatingWord i j (2 * p))).concat i

Tactic:
apply congr_arg

Result:
case pos.h
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ (alternatingWord i j (2 * p))[k] = i

Proof state:
case succ
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
hk : take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
⊢ take (k + 1) (alternatingWord i j (2 * p)) =
    if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)

Tactic:
by_cases h_even : Even k

Result:
case pos
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
hk : take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h_even : Even k
⊢ take (k + 1) (alternatingWord i j (2 * p)) =
    if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)

case neg
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
hk : take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h_even : ¬Even k
⊢ take (k + 1) (alternatingWord i j (2 * p)) =
    if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)