-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem prod_alternatingWord_eq_prod_alternatingWord_sub (i i' : B) (m : ℕ) (hm : m ≤ M i i' * 2) :
    π (alternatingWord i i' m) = π (alternatingWord i' i (M i i' * 2 - m))

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ 2 * k + 1 = 1 + k * 2

Tactic:
ring

Result:
no goals

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
m' : ℤ
⊢ (if Even m' then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m' / 2) =
    (if Even (↑(M.M i i') * 2 - m') then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - m') / 2)

Tactic:
rcases Int.even_or_odd' m' with ⟨k, rfl | rfl⟩

Result:
case intro.inl
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ (if Even (2 * k) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (2 * k / 2) =
    (if Even (↑(M.M i i') * 2 - 2 * k) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - 2 * k) / 2)

case intro.inr
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ (if Even (2 * k + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
    (if Even (↑(M.M i i') * 2 - (2 * k + 1)) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - (2 * k + 1)) / 2)

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this : ¬Even (2 * k + 1)
⊢ ↑(M.M i i') * 2 - (2 * k + 1) = 2 * (↑(M.M i i') - k - 1) + 1

Tactic:
ring

Result:
no goals

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ 2 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
case intro.inl
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ 1 * (cs.simple i * cs.simple i') ^ k = 1 * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') - k) * 2 / 2)

Tactic:
rw [Int.mul_ediv_cancel _ (by norm_num)]

Result:
case intro.inl
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ 1 * (cs.simple i * cs.simple i') ^ k = 1 * (cs.simple i' * cs.simple i) ^ (↑(M.M i i') - k)

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hm : m ≤ M.M i i' * 2
m' : ℤ
⊢ (if Even m' then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m' / ↑2) =
    (if Even (↑(M.M i i' * 2) - m') then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i' * 2) - m') / ↑2)

Tactic:
clear hm

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
m' : ℤ
⊢ (if Even m' then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m' / ↑2) =
    (if Even (↑(M.M i i' * 2) - m') then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i' * 2) - m') / ↑2)

Proof state:
case intro.inr
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this : ¬Even (2 * k + 1)
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
    (if Even (↑(M.M i i') * 2 - (2 * k + 1)) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - (2 * k + 1)) / 2)

Tactic:
have : ¬Even (↑(M i i') * 2 - (2 * k + 1)) :=
  Int.not_even_iff_odd.2 ⟨↑(M i i') - k - 1, by ring⟩

Result:
case intro.inr
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
    (if Even (↑(M.M i i') * 2 - (2 * k + 1)) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - (2 * k + 1)) / 2)

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ ↑(M.M i i') * 2 - (2 * k + 1) = -1 + (-k + ↑(M.M i i')) * 2

Tactic:
ring

Result:
no goals

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hm : m ≤ M.M i i' * 2
⊢ (if Even ↑m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2) =
    (if Even ↑(M.M i i' * 2 - m) then 1 else cs.simple i) * (cs.simple i' * cs.simple i) ^ ((M.M i i' * 2 - m) / 2)

Tactic:
simp_rw [← zpow_natCast, Int.ofNat_ediv, Int.ofNat_sub hm]

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hm : m ≤ M.M i i' * 2
⊢ (if Even ↑m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (↑m / ↑2) =
    (if Even (↑(M.M i i' * 2) - ↑m) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i' * 2) - ↑m) / ↑2)

Proof state:
case intro.inr
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ k =
    cs.simple i * ((cs.simple i' * cs.simple i)⁻¹ ^ 1 * ((cs.simple i' * cs.simple i)⁻¹ ^ k * 1))

Tactic:
simp [← mul_assoc]

Result:
no goals

Proof state:
case intro.inr
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - (2 * k + 1)) / 2)

Tactic:
rw [(by ring : ↑(M i i') * 2 - (2 * k + 1) = -1 + (-k + ↑(M i i')) * 2),
  (by ring : 2 * k + 1 = 1 + k * 2)]

Result:
case intro.inr
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ ((1 + k * 2) / 2) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ ((-1 + (-k + ↑(M.M i i')) * 2) / 2)

Proof state:
case h
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ ↑(M.M i i') * 2 - 2 * k = -k + ↑(M.M i i') + (-k + ↑(M.M i i'))

Tactic:
ring

Result:
no goals

Proof state:
case intro.inl
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ (if Even (2 * k) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (2 * k / 2) =
    (if Even (↑(M.M i i') * 2 - 2 * k) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - 2 * k) / 2)

Tactic:
rw [if_pos (by use k; ring), if_pos (by use -k + (M i i'); ring), mul_comm 2 k, ← sub_mul]

Result:
case intro.inl
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ 1 * (cs.simple i * cs.simple i') ^ (k * 2 / 2) = 1 * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') - k) * 2 / 2)