awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
zero :
  cs.wordProd (alternatingWord i i' 0) =
    (if Even (α := ℕ) 0 then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (0 / 2)
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)
⊢ cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 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]

Premises used: mul_assoc, CoxeterSystem.wordProd_cons, CoxeterSystem.alternatingWord, CoxeterSystem.alternatingWord_succ', Even, pow_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 : ℕ
hm : m ≤ M.M i i' * 2
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)
⊢ cs.wordProd (alternatingWord i i' m) = cs.wordProd (alternatingWord i' i (M.M i i' * 2 - m))

Tactic:
simp_rw [prod_alternatingWord_eq_mul_pow, ← Int.even_coe_nat]

Premises used: CoxeterSystem.prod_alternatingWord_eq_mul_pow, Int.even_coe_nat
-- 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 : ℕ
hm : m ≤ M.M i i' * 2
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 : ℤ))
⊢ (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.natCast_ediv, Int.ofNat_sub hm]

Premises used: zpow_natCast, Int.ofNat_sub, Int.natCast_ediv
-- 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 : ℕ
hm : m ≤ M.M i i' * 2
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 : ℤ))
⊢ (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:
generalize (m : ℤ) = m'

Premises used: Nat.cast
-- 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 : ℕ
m' : ℤ
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)
⊢ (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:
push_cast
-- 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 : ℕ
m' : ℤ
inl :
  ∀ (k : ℤ),
    (if Even (2 * k) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (2 * k / 2) =
      (if Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - 2 * k) then 1 else cs.simple i) *
        (cs.simple i' * cs.simple i) ^ ((HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - 2 * k) / 2)
inr :
  ∀ (k : ℤ),
    (if Even (2 * k + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
      (if Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1)) then 1 else cs.simple i) *
        (cs.simple i' * cs.simple i) ^ ((HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1)) / 2)
⊢ (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:
rcases Int.even_or_odd' m' with ⟨k, rfl | rfl⟩

Premises used: Int.even_or_odd', rfl
-- 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 : ℕ
k : ℤ
h : 2 * k = k + k
⊢ Even (2 * k)

Tactic:
use k
-- 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 : ℕ
k : ℤ
⊢ 2 * k = k + k

Tactic:
ring
-- 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 : ℕ
k : ℤ
h : HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - 2 * k = -k + (↑(M.M i i') : ℤ) + (-k + (↑(M.M i i') : ℤ))
⊢ Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - 2 * k)

Tactic:
use -k + (M i i')

Premises used: CoxeterMatrix.M
-- 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 : ℕ
k : ℤ
⊢ HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - 2 * k = -k + (↑(M.M i i') : ℤ) + (-k + (↑(M.M i i') : ℤ))

Tactic:
ring
-- 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 : ℕ
k : ℤ
inl :
  1 * (cs.simple i * cs.simple i') ^ (k * 2 / 2) = 1 * (cs.simple i' * cs.simple i) ^ (((↑(M.M i i') : ℤ) - k) * 2 / 2)
⊢ (if Even (2 * k) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (2 * k / 2) =
    (if Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - 2 * k) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((HMul.hMul (α := ℤ) (↑(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]

Premises used: if_pos, sub_mul, mul_comm, OfNat.ofNat
-- 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 : ℕ
k : ℤ
⊢ Ne (α := ℤ) 2 0

Tactic:
simp
-- 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 : ℕ
k : ℤ
inl : 1 * (cs.simple i * cs.simple i') ^ k = 1 * (cs.simple i' * cs.simple i) ^ (((↑(M.M i i') : ℤ) - k) * 2 / 2)
⊢ 1 * (cs.simple i * cs.simple i') ^ (k * 2 / 2) = 1 * (cs.simple i' * cs.simple i) ^ (((↑(M.M i i') : ℤ) - k) * 2 / 2)

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

Premises used: Int.mul_ediv_cancel
-- 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 : ℕ
k : ℤ
inl : 1 * (cs.simple i * cs.simple i') ^ k = 1 * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') : ℤ) - 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 simp)]

Premises used: Int.mul_ediv_cancel
-- 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 : ℕ
k : ℤ
inl : 1 * (cs.simple i * cs.simple i') ^ k = 1 * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') : ℤ) - 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)

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

Premises used: Int.mul_ediv_cancel
-- 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 : ℕ
k : ℤ
inl : 1 * (cs.simple i * cs.simple i') ^ k = 1 * (1 * (cs.simple i' * cs.simple i)⁻¹ ^ k)
⊢ 1 * (cs.simple i * cs.simple i') ^ k = 1 * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') : ℤ) - k)

Tactic:
rw [zpow_sub, zpow_natCast, simple_mul_simple_pow' cs i i', ← inv_zpow]

Premises used: zpow_natCast, inv_zpow, CoxeterSystem.simple_mul_simple_pow', zpow_sub
-- 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 : ℕ
k : ℤ
⊢ 1 * (cs.simple i * cs.simple i') ^ k = 1 * (1 * (cs.simple i' * cs.simple i)⁻¹ ^ k)

Tactic:
simp
-- 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 : ℕ
k : ℤ
⊢ ¬Even (2 * k + 1)

Tactic:
have : ¬Even (2 * k + 1) := Int.not_even_iff_odd.2 ⟨k, rfl⟩
-- 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 : ℕ
k : ℤ
this : ¬Even (2 * k + 1)
inr :
  cs.simple i' * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
    (if Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1)) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1)) / 2)
⊢ (if Even (2 * k + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
    (if Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1)) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1)) / 2)

Tactic:
rw [if_neg this]

Premises used: if_neg
-- 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 : ℕ
k : ℤ
this : ¬Even (2 * k + 1)
⊢ HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1) = 2 * ((↑(M.M i i') : ℤ) - k - 1) + 1

Tactic:
ring
-- 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 : ℕ
k : ℤ
this : ¬Even (2 * k + 1)
⊢ ¬Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1))

Tactic:
have : ¬Even (↑(M i i') * 2 - (2 * k + 1)) :=
      Int.not_even_iff_odd.2 ⟨↑(M i i') - k - 1, by ring⟩
-- 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 : ℕ
k : ℤ
this_1 : ¬Even (2 * k + 1)
this : ¬Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1))
inr :
  cs.simple i' * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ ((HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1)) / 2)
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
    (if Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1)) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1)) / 2)

Tactic:
rw [if_neg this]

Premises used: if_neg
-- 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 : ℕ
k : ℤ
this_1 : ¬Even (2 * k + 1)
this : ¬Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1))
⊢ HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1) = -1 + (-k + (↑(M.M i i') : ℤ)) * 2

Tactic:
ring
-- 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 : ℕ
k : ℤ
this_1 : ¬Even (2 * k + 1)
this : ¬Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1))
⊢ 2 * k + 1 = 1 + k * 2

Tactic:
ring
-- 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 : ℕ
k : ℤ
this_1 : ¬Even (2 * k + 1)
this : ¬Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1))
inr :
  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)
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ ((HMul.hMul (α := ℤ) (↑(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)]
-- 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 : ℕ
k : ℤ
this_1 : ¬Even (2 * k + 1)
this : ¬Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1))
⊢ Ne (α := ℤ) 2 0

Tactic:
simp
-- 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 : ℕ
k : ℤ
this_1 : ¬Even (2 * k + 1)
this : ¬Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1))
inr :
  cs.simple i' * (cs.simple i * cs.simple i') ^ (1 / 2 + k) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ ((-1 + (-k + (↑(M.M i i') : ℤ)) * 2) / 2)
⊢ 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)

Tactic:
rw [Int.add_mul_ediv_right _ _ (by simp)]

Premises used: Int.add_mul_ediv_right
-- 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 : ℕ
k : ℤ
this_1 : ¬Even (2 * k + 1)
this : ¬Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1))
inr :
  cs.simple i' * (cs.simple i * cs.simple i') ^ (1 / 2 + k) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ (-1 / 2 + (-k + (↑(M.M i i') : ℤ)))
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ (1 / 2 + k) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ ((-1 + (-k + (↑(M.M i i') : ℤ)) * 2) / 2)

Tactic:
rw [Int.add_mul_ediv_right _ _ (by simp)]

Premises used: Int.add_mul_ediv_right
-- 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 : ℕ
k : ℤ
this_1 : ¬Even (2 * k + 1)
this : ¬Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1))
inr :
  cs.simple i' * (cs.simple i * cs.simple i') ^ (1 / 2 + k) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ (-1 / 2 + (-k + (↑(M.M i i') : ℤ)))
⊢ 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)

Tactic:
repeat rw [Int.add_mul_ediv_right _ _ (by simp)]

Premises used: Int.add_mul_ediv_right
-- 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 : ℕ
k : ℤ
this_1 : ¬Even (2 * k + 1)
this : ¬Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1))
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ (1 / 2 + k) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ (-1 / 2 + (-k + (↑(M.M i i') : ℤ)))

Tactic:
simp [zpow_add, simple_mul_simple_pow', ← inv_zpow, ← mul_assoc]

Premises used: zpow_add, mul_assoc, inv_zpow, CoxeterSystem.simple_mul_simple_pow'
-- 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
⊢ LT.lt (α := ℕ) 0 2

Tactic:
simp
-- 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' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i i' * 2 - M.M i i'))

Tactic:
have := cs.prod_alternatingWord_eq_prod_alternatingWord_sub i i' (M i i')
    (Nat.le_mul_of_pos_right _ (by simp))
-- 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
this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i i' * 2 - M.M i i'))
⊢ cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i i'))

Tactic:
rw [tsub_eq_of_eq_add (mul_two (M i i'))] at this

Premises used: CoxeterMatrix.M, tsub_eq_of_eq_add, mul_two
-- 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
this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i i'))
⊢ cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i' i))

Tactic:
nth_rw 2 [M.symmetric i i'] at this

Premises used: CoxeterMatrix.symmetric
-- 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
this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i' i))
⊢ cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)

Tactic:
this
-- 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
this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i' i))
⊢ cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)

Tactic:
exact this
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
h : cs.simple i = 1 * cs.simple i * 1⁻¹
⊢ cs.IsReflection (cs.simple i)

Tactic:
use 1, i
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.simple i = 1 * cs.simple i * 1⁻¹

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
rcases : ∀ (w : W) (i : B), HPow.hPow (β := ℕ) (w * cs.simple i * w⁻¹) 2 = 1
⊢ HPow.hPow (β := ℕ) t 2 = 1

Tactic:
rcases ht with ⟨w, i, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ HPow.hPow (β := ℕ) (w * cs.simple i * w⁻¹) 2 = 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
rcases : ∀ (w : W) (i : B), w * cs.simple i * w⁻¹ * (w * cs.simple i * w⁻¹) = 1
⊢ t * t = 1

Tactic:
rcases ht with ⟨w, i, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ w * cs.simple i * w⁻¹ * (w * cs.simple i * w⁻¹) = 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
rcases : ∀ (w : W) (i : B), (w * cs.simple i * w⁻¹)⁻¹ = w * cs.simple i * w⁻¹
⊢ t⁻¹ = t

Tactic:
rcases ht with ⟨w, i, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ (w * cs.simple i * w⁻¹)⁻¹ = w * cs.simple i * w⁻¹

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht rwa rwa₁ rwa₂ rwa₃ : cs.IsReflection t
⊢ cs.IsReflection t⁻¹

Tactic:
rwa [ht.inv]

Premises used: CoxeterSystem.IsReflection.inv
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
this :
  Eq (α := Multiplicative (ZMod 2)) ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) t : Multiplicative (ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 1 : Multiplicative (ZMod 2))
⊢ Odd (cs.length t)

Tactic:
simpa [lengthParity_eq_ofAdd_length, ZMod.natCast_eq_one_iff_odd]

Premises used: ZMod.natCast_eq_one_iff_odd, CoxeterSystem.lengthParity_eq_ofAdd_length
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
suffices :
  Eq (α := Multiplicative (ZMod 2)) ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) t : Multiplicative (ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 1 : Multiplicative (ZMod 2))
⊢ Odd (cs.length t)

Tactic:
suffices cs.lengthParity t = Multiplicative.ofAdd 1 by
    simpa [lengthParity_eq_ofAdd_length, ZMod.natCast_eq_one_iff_odd]
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
rcases :
  ∀ (w : W) (i : B),
    Eq (α := Multiplicative (ZMod 2))
      ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (w * cs.simple i * w⁻¹) : Multiplicative (ZMod 2))
      ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 1 : Multiplicative (ZMod 2))
⊢ Eq (α := Multiplicative (ZMod 2)) ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) t : Multiplicative (ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 1 : Multiplicative (ZMod 2))

Tactic:
rcases ht with ⟨w, i, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ Eq (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (w * cs.simple i * w⁻¹) : Multiplicative (ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 1 : Multiplicative (ZMod 2))

Tactic:
simp [lengthParity_simple]

Premises used: CoxeterSystem.lengthParity_simple
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
this :
  Ne (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (w * t) : Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))
contrapose :
  ∀ (this : cs.length (w * t) = cs.length w),
    Eq (α := Multiplicative (ZMod 2))
      ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (w * t) : Multiplicative (ZMod 2))
      ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))
⊢ cs.length (w * t) ≠ cs.length w

Tactic:
contrapose this
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
this : cs.length (w * t) = cs.length w
⊢ Eq (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (w * t) : Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))

Tactic:
simp only [lengthParity_eq_ofAdd_length, this]

Premises used: CoxeterSystem.lengthParity_eq_ofAdd_length