awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (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)
have 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)
Tactic: rcases Int.even_or_odd' m' with ⟨k, rfl | rfl⟩
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 : ℕ
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)
⊢ (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)
have 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)
Tactic: rcases Int.even_or_odd' m' with ⟨k, rfl | rfl⟩
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 : ℕ
k : ℤ
⊢ Even (2 * k)
have h : 2 * k = k + k
Tactic: use k
-- 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 : ℕ
k : ℤ
⊢ Even (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - 2 * k)
have h : HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - 2 * k = -k + (↑(M.M i i') : ℤ) + (-k + (↑(M.M i i') : ℤ))
Tactic: use -k + (M i i')
-- 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 : ℕ
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)
have 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)
Tactic: rw [if_pos (by use k; ring), if_pos (by use -k + (M i i'); ring), mul_comm 2 k, ← sub_mul]
-- 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 : ℕ
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)
have inl : 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)]
-- 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 : ℕ
k : ℤ
⊢ 1 * (cs.simple i * cs.simple i') ^ k = 1 * (cs.simple i' * cs.simple i) ^ (((↑(M.M i i') : ℤ) - k) * 2 / 2)
have inl : 1 * (cs.simple i * cs.simple i') ^ k = 1 * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') : ℤ) - k)
Tactic: rw [Int.mul_ediv_cancel _ (by simp)]
-- 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 : ℕ
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)
have inl : 1 * (cs.simple i * cs.simple i') ^ k = 1 * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') : ℤ) - k)
Tactic: repeat rw [Int.mul_ediv_cancel _ (by simp)]
-- 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 : ℕ
k : ℤ
⊢ 1 * (cs.simple i * cs.simple i') ^ k = 1 * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') : ℤ) - k)
have inl : 1 * (cs.simple i * cs.simple i') ^ k = 1 * (1 * (cs.simple i' * cs.simple i)⁻¹ ^ k)
Tactic: rw [zpow_sub, zpow_natCast, simple_mul_simple_pow' cs i i', ← inv_zpow]
-- 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 : ℕ
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)
have this : ¬Even (2 * k + 1)
Tactic: have : ¬Even (2 * k + 1) := Int.not_even_iff_odd.2 ⟨k, rfl⟩
-- 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 : ℕ
k : ℤ
this : ¬Even (2 * k + 1)
⊢ (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)
have 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)
Tactic: rw [if_neg this]
-- 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 : ℕ
k : ℤ
this : ¬Even (2 * k + 1)
⊢ 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)
have this₁ : ¬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⟩
-- 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 : ℕ
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') ^ ((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)
have 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)
Tactic: rw [if_neg this]
-- 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 : ℕ
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') ^ ((2 * k + 1) / 2) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ ((HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 - (2 * k + 1)) / 2)
have 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)
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)]
-- 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 : ℕ
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 + k * 2) / 2) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ ((-1 + (-k + (↑(M.M i i') : ℤ)) * 2) / 2)
have 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)
Tactic: rw [Int.add_mul_ediv_right _ _ (by simp)]
-- 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 : ℕ
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 + (-k + (↑(M.M i i') : ℤ)) * 2) / 2)
have 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') : ℤ)))
Tactic: rw [Int.add_mul_ediv_right _ _ (by simp)]
-- 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 : ℕ
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 + k * 2) / 2) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ ((-1 + (-k + (↑(M.M i i') : ℤ)) * 2) / 2)
have 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') : ℤ)))
Tactic: repeat rw [Int.add_mul_ediv_right _ _ (by simp)]
-- 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
⊢ cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)
have this : 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))
-- 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
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 (braidWord M i i') = cs.wordProd (braidWord M i' i)
have this₁ : 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
Cleared hypotheses: this
-- 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
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)
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.IsReflection (cs.simple i)
have h : cs.simple i = 1 * cs.simple i * 1⁻¹
Tactic: use 1, i
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
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
⊢ HPow.hPow (β := ℕ) t 2 = 1
have rcases : ∀ (w : W) (i : B), HPow.hPow (β := ℕ) (w * cs.simple i * w⁻¹) 2 = 1
Tactic: rcases ht with ⟨w, i, rfl⟩
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
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
⊢ t * t = 1
have rcases : ∀ (w : W) (i : B), w * cs.simple i * w⁻¹ * (w * cs.simple i * w⁻¹) = 1
Tactic: rcases ht with ⟨w, i, rfl⟩
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
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
⊢ t⁻¹ = t
have rcases : ∀ (w : W) (i : B), (w * cs.simple i * w⁻¹)⁻¹ = w * cs.simple i * w⁻¹
Tactic: rcases ht with ⟨w, i, rfl⟩
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
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
⊢ Odd (cs.length t)
have 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))
Tactic: suffices cs.lengthParity t = Multiplicative.ofAdd 1 by
    simpa [lengthParity_eq_ofAdd_length, ZMod.natCast_eq_one_iff_odd]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
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
⊢ 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))
have 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))
Tactic: rcases ht with ⟨w, i, rfl⟩
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
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))
⊢ cs.length (w * t) ≠ cs.length w
have 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))
Tactic: contrapose this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
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
⊢ cs.length (w * t) ≠ cs.length w
have suffices : 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))
Tactic: suffices cs.lengthParity (w * t) ≠ cs.lengthParity w by
    contrapose this
    simp only [lengthParity_eq_ofAdd_length, this]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
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
⊢ 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))
have rcases : ∀ (w_1 : W) (i : B),
  Ne (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (w * (w_1 * cs.simple i * w_1⁻¹)) : Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))
Tactic: rcases ht with ⟨w, i, rfl⟩
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
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)) (t * w) : Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))
⊢ cs.length (t * w) ≠ cs.length w
have contrapose : ∀ (this : cs.length (t * w) = cs.length w),
  Eq (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (t * w) : Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))
Tactic: contrapose this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
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
⊢ cs.length (t * w) ≠ cs.length w
have suffices : Ne (α := Multiplicative (ZMod 2))
  ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (t * w) : Multiplicative (ZMod 2))
  ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))
Tactic: suffices cs.lengthParity (t * w) ≠ cs.lengthParity w by
    contrapose this
    simp only [lengthParity_eq_ofAdd_length, this]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
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
⊢ Ne (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (t * w) : Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))
have rcases : ∀ (w_1 : W) (i : B),
  Ne (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (w_1 * cs.simple i * w_1⁻¹ * w) : Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))
Tactic: rcases ht with ⟨w, i, rfl⟩
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
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
⊢ cs.IsReflection (w * t * w⁻¹)
have obtain : ∀ (u : W) (i : B), cs.IsReflection (w * (u * cs.simple i * u⁻¹) * w⁻¹)
Tactic: obtain ⟨u, i, rfl⟩ := ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w u : W
i : B
⊢ cs.IsReflection (w * (u * cs.simple i * u⁻¹) * w⁻¹)
have h : w * (u * cs.simple i * u⁻¹) * w⁻¹ = w * u * cs.simple i * (w * u)⁻¹
Tactic: use w * u, i
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsReflection (w * t * w⁻¹) ↔ cs.IsReflection t
have mp : cs.IsReflection (w * t * w⁻¹) → cs.IsReflection t
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
mp : cs.IsReflection (w * t * w⁻¹) → cs.IsReflection t
⊢ cs.IsReflection (w * t * w⁻¹) ↔ cs.IsReflection t
have mpr : cs.IsReflection t → cs.IsReflection (w * t * w⁻¹)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsRightInversion w⁻¹ t ↔ cs.IsLeftInversion w t
have h : cs.IsReflection t → (cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w)
Tactic: apply and_congr_right
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
ht : cs.IsReflection t
⊢ cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
have h : cs.length (w⁻¹ * t)⁻¹ < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
Tactic: rw [← length_inv, mul_inv_rev, inv_inv, ht.inv, cs.length_inv w]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
ht : cs.IsReflection t
h : cs.length (w⁻¹ * t)⁻¹ < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
⊢ cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
have h₁ : cs.length (t⁻¹ * w⁻¹⁻¹) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
Tactic: rw [← length_inv, mul_inv_rev, inv_inv, ht.inv, cs.length_inv w]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
ht : cs.IsReflection t
h : cs.length (w⁻¹ * t)⁻¹ < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
h₁ : cs.length (t⁻¹ * w⁻¹⁻¹) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
⊢ cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
have h₂ : cs.length (t⁻¹ * w) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
Tactic: rw [← length_inv, mul_inv_rev, inv_inv, ht.inv, cs.length_inv w]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
ht : cs.IsReflection t
h : cs.length (w⁻¹ * t)⁻¹ < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
h₁ : cs.length (t⁻¹ * w⁻¹⁻¹) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
h₂ : cs.length (t⁻¹ * w) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
⊢ cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
have h₃ : cs.length (t * w) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
Tactic: rw [← length_inv, mul_inv_rev, inv_inv, ht.inv, cs.length_inv w]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
ht : cs.IsReflection t
h : cs.length (w⁻¹ * t)⁻¹ < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
h₁ : cs.length (t⁻¹ * w⁻¹⁻¹) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
h₂ : cs.length (t⁻¹ * w) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
h₃ : cs.length (t * w) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
⊢ cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
have h₄ : cs.length (t * w) < cs.length w ↔ cs.length (t * w) < cs.length w
Tactic: rw [← length_inv, mul_inv_rev, inv_inv, ht.inv, cs.length_inv w]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsLeftInversion w⁻¹ t ↔ cs.IsRightInversion w t
have h : w = w⁻¹⁻¹
Tactic: convert! cs.isRightInversion_inv_iff.symm
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
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
⊢ cs.IsReflection t ∧ cs.length (w * t * t) < cs.length (w * t) ↔ ¬(cs.IsReflection t ∧ cs.length (w * t) < cs.length w)
have simp : cs.length w < cs.length (w * t) ↔ cs.length w ≤ cs.length (w * t)
Tactic: simp only [mul_assoc, ht.mul_self, mul_one, ht, true_and, not_lt]