awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
pos : ∀ (h_even : Even (p + k)), (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i
neg : ∀ (h_even : ¬Even (p + k)), (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i

Tactic:
by_cases h_even : Even (p + k)

Premises used: HAdd.hAdd, Even
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : Even (p + k)
pos : (if Even (p + k + 1) then i else j) = j
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i

Tactic:
rw [if_pos h_even, ← add_assoc]

Premises used: add_assoc, if_pos
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : Even (p + k)
⊢ (if Even (p + k + 1) then i else j) = j

Tactic:
simp only [ite_eq_right_iff, isEmpty_Prop, Nat.not_even_iff_odd, Even.add_one h_even,
      IsEmpty.forall_iff]

Premises used: Even.add_one, Nat.not_even_iff_odd, ite_eq_right_iff, isEmpty_Prop, IsEmpty.forall_iff
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : ¬Even (p + k)
neg : (if Even (p + k + 1) then i else j) = i
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i

Tactic:
rw [if_neg h_even, ← add_assoc]

Premises used: add_assoc, if_neg
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : ¬Even (p + k)
⊢ (if Even (p + k + 1) then i else j) = i

Tactic:
simp [Odd.add_one (Nat.not_even_iff_odd.mp h_even)]

Premises used: Nat.not_even_iff_odd, Iff.mp, Odd.add_one
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p : ℕ
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:
simp only [take_zero, Even.zero, ↓reduceIte, alternatingWord]

Premises used: Even.zero, List.take_zero, CoxeterSystem.alternatingWord, reduceIte
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
⊢ k < 2 * p

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
⊢ k < 2 * p

Tactic:
have hk : k < 2 * p := by lia
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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 : k < 2 * p
⊢ take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k

Tactic:
apply h' at hk
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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)
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)
⊢ 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

Premises used: Even
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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 (alternatingWord i j (2 * p)) = alternatingWord i j k

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

Premises used: reduceIte
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
pos : take (k + 1) (alternatingWord i j (2 * p)) = 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)

Tactic:
simp only [Nat.not_even_iff_odd.mpr (Even.add_one h_even), ↓reduceIte]

Premises used: Iff.mpr, Even.add_one, Nat.not_even_iff_odd, reduceIte
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
simp : k < 2 * p
⊢ k < (alternatingWord i j (2 * p)).length

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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 < 2 * p

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
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 ⋯) =
    (take k (alternatingWord i j (2 * p))).concat i
⊢ take (k + 1) (alternatingWord i j (2 * p)) = alternatingWord j i (k + 1)

Tactic:
rw [← List.take_concat_get (by simp; lia), alternatingWord_succ, ← hk]

Premises used: List.take_concat_get, CoxeterSystem.alternatingWord_succ
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
pos : getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) k ⋯ = i
⊢ (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

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
pos : (if Even (2 * p + k) then i else j) = i
⊢ getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) k ⋯ = i

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

Premises used: HMul.hMul, CoxeterSystem.getElem_alternatingWord, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
apply : Even (2 * p) ↔ Even k
⊢ Even (2 * p + k)

Tactic:
apply Nat.even_add.mpr

Premises used: Iff.mpr, Nat.even_add
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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) ↔ Even k

Tactic:
simp [h_even]
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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 (alternatingWord i j (2 * p)) = alternatingWord j i k

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

Premises used: reduceIte
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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 k

Tactic:
simpa using h_even
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
neg : take (k + 1) (alternatingWord i j (2 * p)) = alternatingWord i j (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)

Tactic:
simp only [Odd.add_one (by simpa using h_even), ↓reduceIte]

Premises used: reduceIte, Odd.add_one
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
simp : k < 2 * p
⊢ k < (alternatingWord i j (2 * p)).length

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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 < 2 * p

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
neg :
  (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
⊢ take (k + 1) (alternatingWord i j (2 * p)) = alternatingWord i j (k + 1)

Tactic:
rw [← List.take_concat_get (by simp; lia), alternatingWord_succ, hk]

Premises used: List.take_concat_get, CoxeterSystem.alternatingWord_succ
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
neg : getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) k ⋯ = j
⊢ (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

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
neg : (if Even (2 * p + k) then i else j) = j
⊢ getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) k ⋯ = j

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

Premises used: HMul.hMul, CoxeterSystem.getElem_alternatingWord, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
apply : Odd (2 * p) ↔ Even k
⊢ Odd (2 * p + k)

Tactic:
apply Nat.odd_add.mpr

Premises used: Iff.mpr, Nat.odd_add
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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) ↔ Even k

Tactic:
simp [h_even]
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
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)
⊢ take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k

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))]

Premises used: HMul.hMul, Even.zero, List.take_zero, CoxeterSystem.getElem_alternatingWord, CoxeterSystem.alternatingWord, congr_arg, Even, reduceIte, Odd.add_one, OfNat.ofNat, List.take_concat_get, CoxeterSystem.alternatingWord_succ
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k < 2 * p

Tactic:
lia
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
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
⊢ take (k + 1) (alternatingWord i j (2 * p)) = i :: take k (alternatingWord j i (2 * p))

Tactic:
rw [listTake_alternatingWord j i p k (by lia), listTake_alternatingWord i j p (k + 1) h]

Premises used: HAdd.hAdd, CoxeterSystem.listTake_alternatingWord, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
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
⊢ (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

Premises used: Even
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
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:
simp [Nat.not_even_iff_odd.mpr (Even.add_one h_even), alternatingWord_succ', h_even]

Premises used: Iff.mpr, Even.add_one, Nat.not_even_iff_odd, CoxeterSystem.alternatingWord_succ'
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
h_even : ¬Even k
⊢ Odd k

Tactic:
rw [Nat.not_even_iff_odd] at h_even

Premises used: Nat.not_even_iff_odd
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
h_even : Odd k
⊢ Even (k + 1)

Tactic:
Odd.add_one h_even

Premises used: Odd.add_one
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
h_even : Odd k
⊢ Even (k + 1)

Tactic:
exact Odd.add_one h_even

Premises used: Odd.add_one
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
⊢ cs.wordProd (alternatingWord i i' 0) =
    (if Even (α := ℕ) 0 then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (0 / 2)

Tactic:
simp [alternatingWord]

Premises used: CoxeterSystem.alternatingWord
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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)
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)
⊢ 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:
rw [alternatingWord_succ', wordProd_cons, ih]

Premises used: CoxeterSystem.wordProd_cons, CoxeterSystem.alternatingWord_succ'
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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)
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)
⊢ 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

Premises used: Even
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
⊢ ¬Even (m + 1)

Tactic:
simp [hm, parity_simps]
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
⊢ ¬Even (m + 1)

Tactic:
have h₁ : ¬ Even (m + 1) := by simp [hm, parity_simps]
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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)
rwa rwa₁ rwa₂ rwa₃ : ¬Even (m + 1)
⊢ ¬2 ∣ m + 1

Tactic:
rwa [← even_iff_two_dvd]

Premises used: even_iff_two_dvd
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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)
⊢ (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]
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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)
h₂ : (m + 1) / 2 = 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)

Tactic:
simp [hm, h₁, h₂]
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
⊢ Even (m + 1)

Tactic:
simp [hm, parity_simps]
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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
⊢ Even (m + 1)

Tactic:
have h₁ : Even (m + 1) := by simp [hm, parity_simps]
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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)
⊢ (m + 1) / 2 = m / 2 + 1

Tactic:
have h₂ : (m + 1) / 2 = m / 2 + 1 := Nat.succ_div_of_dvd h₁.two_dvd
-- Module: Mathlib.GroupTheory.Coxeter.Basic
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)
h₂ : (m + 1) / 2 = m / 2 + 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)

Tactic:
simp [hm, h₁, h₂, ← pow_succ', ← mul_assoc]

Premises used: mul_assoc, pow_succ'