awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (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
pos :
  ∀ (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)
⊢ take (k + 1) (alternatingWord i j (2 * p)) =
    if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)
have neg : ∀ (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: by_cases h_even : Even k
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (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)
have hk₁ : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
Tactic: simp only [h_even, ↓reduceIte] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (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)
have pos : take (k + 1) (alternatingWord i j (2 * p)) = alternatingWord j i (k + 1)
Tactic: simp only [Nat.not_even_iff_odd.mpr (Even.add_one h_even), ↓reduceIte]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (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
have simp : k < 2 * p
Tactic: simp
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (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)) = alternatingWord j i (k + 1)
have pos : (take k (alternatingWord i j (2 * p))).concat
    (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) k sorry) =
  (take k (alternatingWord i j (2 * p))).concat i
Tactic: rw [← List.take_concat_get (by simp; lia), alternatingWord_succ, ← hk]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (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
      (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) k ⋯) =
    (take k (alternatingWord i j (2 * p))).concat i
have pos : getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) k sorry = i
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (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
⊢ getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) k ⋯ = i
have pos : (if Even (2 * p + k) then i else j) = i
Tactic: rw [getElem_alternatingWord i j (2 * p) k (by lia)]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (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)
have apply : Even (2 * p) ↔ Even k
Tactic: apply Nat.even_add.mpr
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (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)
have hk₁ : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
Tactic: simp only [h_even, ↓reduceIte] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (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)
have neg : take (k + 1) (alternatingWord i j (2 * p)) = alternatingWord i j (k + 1)
Tactic: simp only [Odd.add_one (by simpa using h_even), ↓reduceIte]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (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
have simp : k < 2 * p
Tactic: simp
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (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)) = alternatingWord i j (k + 1)
have neg : (alternatingWord j i k).concat
    (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) k sorry) =
  (alternatingWord j i k).concat j
Tactic: rw [← List.take_concat_get (by simp; lia), alternatingWord_succ, hk]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (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
⊢ (alternatingWord j i k).concat
      (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) k ⋯) =
    (alternatingWord j i k).concat j
have neg : getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) k sorry = j
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (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
⊢ getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) k ⋯ = j
have neg : (if Even (2 * p + k) then i else j) = j
Tactic: rw [getElem_alternatingWord i j (2 * p) k (by lia)]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h' :
  ∀ (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)
have apply : Odd (2 * p) ↔ Even k
Tactic: apply Nat.odd_add.mpr
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
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
have zero : ∀ (h : 0 < 2 * p),
  take 0 (alternatingWord i j (2 * p)) = if Even (α := ℕ) 0 then alternatingWord i j 0 else alternatingWord j i 0
Tactic: induction k with
    | zero =>
      simp only [take_zero, Even.zero, ↓reduceIte, alternatingWord]
    | succ k h' =>
      have hk : k < 2 * p := by lia
      apply h' at hk
      by_cases h_even : Even k
      · simp only [h_even, ↓reduceIte] at hk
        simp only [Nat.not_even_iff_odd.mpr (Even.add_one h_even), ↓reduceIte]
        rw [← List.take_concat_get (by simp; lia), alternatingWord_succ, ← hk]
        apply congr_arg
        rw [getElem_alternatingWord i j (2 * p) k (by lia)]
        simp [(by apply Nat.even_add.mpr; simp [h_even] : Even (2 * p + k))]
      · simp only [h_even, ↓reduceIte] at hk
        simp only [Odd.add_one (by simpa using h_even), ↓reduceIte]
        rw [← List.take_concat_get (by simp; lia), alternatingWord_succ, hk]
        apply congr_arg
        rw [getElem_alternatingWord i j (2 * p) k (by lia)]
        simp [(by apply Nat.odd_add.mpr; simp [h_even] : Odd (2 * p + k))]
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k < 2 * p
zero :
  ∀ (h : 0 < 2 * p),
    take 0 (alternatingWord i j (2 * p)) = if Even (α := ℕ) 0 then alternatingWord i j 0 else alternatingWord j i 0
⊢ take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
have succ : ∀ (k : ℕ)
  (h' :
    ∀ (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),
  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: induction k with
    | zero =>
      simp only [take_zero, Even.zero, ↓reduceIte, alternatingWord]
    | succ k h' =>
      have hk : k < 2 * p := by lia
      apply h' at hk
      by_cases h_even : Even k
      · simp only [h_even, ↓reduceIte] at hk
        simp only [Nat.not_even_iff_odd.mpr (Even.add_one h_even), ↓reduceIte]
        rw [← List.take_concat_get (by simp; lia), alternatingWord_succ, ← hk]
        apply congr_arg
        rw [getElem_alternatingWord i j (2 * p) k (by lia)]
        simp [(by apply Nat.even_add.mpr; simp [h_even] : Even (2 * p + k))]
      · simp only [h_even, ↓reduceIte] at hk
        simp only [Odd.add_one (by simpa using h_even), ↓reduceIte]
        rw [← List.take_concat_get (by simp; lia), alternatingWord_succ, hk]
        apply congr_arg
        rw [getElem_alternatingWord i j (2 * p) k (by lia)]
        simp [(by apply Nat.odd_add.mpr; simp [h_even] : Odd (2 * p + k))]
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ take (k + 1) (alternatingWord i j (2 * p)) = i :: take k (alternatingWord j i (2 * p))
have rw : (if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)) =
  i :: if Even k then alternatingWord j i k else alternatingWord i j k
Tactic: rw [listTake_alternatingWord j i p k (by lia), listTake_alternatingWord i j p (k + 1) h]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ (if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)) =
    i :: if Even k then alternatingWord j i k else alternatingWord i j k
have pos : ∀ (h_even : Even k),
  (if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)) =
    i :: if Even k then alternatingWord j i k else alternatingWord i j k
Tactic: by_cases h_even : Even k
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
pos :
  ∀ (h_even : Even k),
    (if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)) =
      i :: if Even k then alternatingWord j i k else alternatingWord i j k
⊢ (if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)) =
    i :: if Even k then alternatingWord j i k else alternatingWord i j k
have neg : ∀ (h_even : ¬Even k),
  (if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)) =
    i :: if Even k then alternatingWord j i k else alternatingWord i j k
Tactic: by_cases h_even : Even k
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
h_even : ¬Even k
⊢ Even (k + 1)
have h_even₁ : Odd k
Tactic: rw [Nat.not_even_iff_odd] at h_even
Cleared hypotheses: h_even
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
⊢ cs.wordProd (alternatingWord i i' (m + 1)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)
have succ : cs.simple (if Even m then i' else i) * ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
  (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)
Tactic: rw [alternatingWord_succ', wordProd_cons, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
⊢ cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)
have pos : ∀ (hm : Even m),
  cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)
Tactic: by_cases hm : Even m
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
pos :
  ∀ (hm : Even m),
    cs.simple (if Even m then i' else i) *
        ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
      (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)
⊢ cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)
have neg : ∀ (hm : ¬Even m),
  cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)
Tactic: by_cases hm : Even m
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
hm : Even m
⊢ cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)
have h₁ : ¬Even (m + 1)
Tactic: have h₁ : ¬ Even (m + 1) := by simp [hm, parity_simps]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
hm : Even m
h₁ : ¬Even (m + 1)
⊢ cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)
have h₂ : (m + 1) / 2 = m / 2
Tactic: have h₂ : (m + 1) / 2 = m / 2 := Nat.succ_div_of_not_dvd <| by rwa [← even_iff_two_dvd]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
hm : ¬Even m
⊢ cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)
have h₁ : Even (m + 1)
Tactic: have h₁ : Even (m + 1) := by simp [hm, parity_simps]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
hm : ¬Even m
h₁ : Even (m + 1)
⊢ cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)
have h₂ : (m + 1) / 2 = m / 2 + 1
Tactic: have h₂ : (m + 1) / 2 = m / 2 + 1 := Nat.succ_div_of_dvd h₁.two_dvd
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
⊢ cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
have zero : cs.wordProd (alternatingWord i i' 0) =
  (if Even (α := ℕ) 0 then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (0 / 2)
Tactic: induction m with
  | zero => simp [alternatingWord]
  | succ m ih =>
    rw [alternatingWord_succ', wordProd_cons, ih]
    by_cases hm : Even m
    · have h₁ : ¬ Even (m + 1) := by simp [hm, parity_simps]
      have h₂ : (m + 1) / 2 = m / 2 := Nat.succ_div_of_not_dvd <| by rwa [← even_iff_two_dvd]
      simp [hm, h₁, h₂]
    · have h₁ : Even (m + 1) := by simp [hm, parity_simps]
      have h₂ : (m + 1) / 2 = m / 2 + 1 := Nat.succ_div_of_dvd h₁.two_dvd
      simp [hm, h₁, h₂, ← pow_succ', ← mul_assoc]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
zero :
  cs.wordProd (alternatingWord i i' 0) =
    (if Even (α := ℕ) 0 then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (0 / 2)
⊢ cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
have succ : ∀ (m : ℕ)
  (ih :
    cs.wordProd (alternatingWord i i' m) =
      (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)),
  cs.wordProd (alternatingWord i i' (m + 1)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)
Tactic: induction m with
  | zero => simp [alternatingWord]
  | succ m ih =>
    rw [alternatingWord_succ', wordProd_cons, ih]
    by_cases hm : Even m
    · have h₁ : ¬ Even (m + 1) := by simp [hm, parity_simps]
      have h₂ : (m + 1) / 2 = m / 2 := Nat.succ_div_of_not_dvd <| by rwa [← even_iff_two_dvd]
      simp [hm, h₁, h₂]
    · have h₁ : Even (m + 1) := by simp [hm, parity_simps]
      have h₂ : (m + 1) / 2 = m / 2 + 1 := Nat.succ_div_of_dvd h₁.two_dvd
      simp [hm, h₁, h₂, ← pow_succ', ← mul_assoc]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
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
⊢ cs.wordProd (alternatingWord i i' m) = cs.wordProd (alternatingWord i' i (M.M i i' * 2 - m))
have simp_rw : (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 [prod_alternatingWord_eq_mul_pow, ← Int.even_coe_nat]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
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)
have simp_rw : (if Even (α := ℤ) (↑m : ℤ) then 1 else cs.simple i') *
    (cs.simple i * cs.simple i') ^ HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑2 : ℤ) =
  (if Even (HSub.hSub (α := ℤ) (↑(M.M i i' * 2) : ℤ) (↑m : ℤ)) then 1 else cs.simple i) *
    (cs.simple i' * cs.simple i) ^ (HSub.hSub (α := ℤ) (↑(M.M i i' * 2) : ℤ) (↑m : ℤ) / (↑2 : ℤ))
Tactic: simp_rw [← zpow_natCast, Int.natCast_ediv, Int.ofNat_sub hm]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
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') ^ HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑2 : ℤ) =
    (if Even (HSub.hSub (α := ℤ) (↑(M.M i i' * 2) : ℤ) (↑m : ℤ)) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ (HSub.hSub (α := ℤ) (↑(M.M i i' * 2) : ℤ) (↑m : ℤ) / (↑2 : ℤ))
have generalize : ∀ (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: generalize (m : ℤ) = m'
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
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 : ℤ))
have push_cast : (if Even m' then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m' / 2) =
  (if Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - m') then 1 else cs.simple i) *
    (cs.simple i' * cs.simple i) ^ ((HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - m') / 2)
Tactic: push_cast