awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p k : ℕ
hk :
  ∀ (i j : B) (h : k < 2 * p),
    getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq (alternatingWord i j (2 * p))) k ⋯ =
      cs.wordProd (alternatingWord j i (2 * k + 1))
i j : B
h : k + 1 < 2 * p
⊢ 2 * (k + 1) = 2 * k + 1 + 1

Tactic:
ring
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p k : ℕ
hk :
  ∀ (i j : B) (h : k < 2 * p),
    getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq (alternatingWord i j (2 * p))) k ⋯ =
      cs.wordProd (alternatingWord j i (2 * k + 1))
i j : B
h : k + 1 < 2 * p
succ :
  cs.simple i * cs.wordProd (alternatingWord i j (2 * k + 1)) * cs.simple i =
    cs.simple i * (cs.wordProd (alternatingWord i j (2 * k + 1)) * cs.simple i)
⊢ cs.simple i * cs.wordProd (alternatingWord i j (2 * k + 1)) * cs.simple i =
    cs.simple i * cs.wordProd (alternatingWord j i (2 * (k + 1)))

Tactic:
rw [(by ring : 2 * (k + 1) = 2 * k + 1 + 1), alternatingWord_succ j i, wordProd_concat]

Premises used: CoxeterSystem.wordProd_concat, CoxeterSystem.alternatingWord_succ
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p k : ℕ
hk :
  ∀ (i j : B) (h : k < 2 * p),
    getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq (alternatingWord i j (2 * p))) k ⋯ =
      cs.wordProd (alternatingWord j i (2 * k + 1))
i j : B
h : k + 1 < 2 * p
⊢ cs.simple i * cs.wordProd (alternatingWord i j (2 * k + 1)) * cs.simple i =
    cs.simple i * (cs.wordProd (alternatingWord i j (2 * k + 1)) * cs.simple i)

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
i j : B
p k : ℕ
h : k < 2 * p
zero :
  ∀ (i j : B) (h : 0 < 2 * p),
    getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq (alternatingWord i j (2 * p))) 0 ⋯ =
      cs.wordProd (alternatingWord j i (HMul.hMul (α := ℕ) 2 0 + 1))
succ :
  ∀ (k : ℕ)
    (hk :
      ∀ (i j : B) (h : k < 2 * p),
        getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq (alternatingWord i j (2 * p))) k ⋯ =
          cs.wordProd (alternatingWord j i (2 * k + 1)))
    (i j : B) (h : k + 1 < 2 * p),
    getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq (alternatingWord i j (2 * p))) (k + 1)
        ⋯ =
      cs.wordProd (alternatingWord j i (2 * (k + 1) + 1))
⊢ getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq (alternatingWord i j (2 * p))) k ⋯ =
    cs.wordProd (alternatingWord j i (2 * k + 1))

Tactic:
induction k generalizing i j with
  | zero =>
    simp only [CoxeterSystem.getElem_leftInvSeq cs (alternatingWord i j (2 * p)) 0 (by simp [h]),
      take_zero, wordProd_nil, one_mul, inv_one, mul_one, alternatingWord, concat_eq_append,
      nil_append, wordProd_singleton]
    simp only [getElem_alternatingWord i j (2 * p) 0 (by simp [h]), add_zero, even_two,
      Even.mul_right, ↓reduceIte]
  | succ k hk =>
    simp only [getElem_succ_leftInvSeq_alternatingWord cs i j p k h, hk _ _ (by lia),
      MulAut.conj_apply, inv_simple, alternatingWord_succ' j i, even_two, Even.mul_right,
      ↓reduceIte, wordProd_cons]
    rw [(by ring : 2 * (k + 1) = 2 * k + 1 + 1), alternatingWord_succ j i, wordProd_concat]
    simp [mul_assoc]

Premises used: CoxeterSystem.inv_simple, HMul.hMul, inv_one, even_two, mul_assoc, CoxeterSystem.wordProd_cons, List.take_zero, Even.mul_right, CoxeterSystem.getElem_alternatingWord, CoxeterSystem.wordProd_concat, CoxeterSystem.alternatingWord, MulAut.conj_apply, List.concat_eq_append, CoxeterSystem.wordProd_singleton, CoxeterSystem.wordProd_nil, CoxeterSystem.alternatingWord_succ', List.nil_append, reduceIte, mul_one, add_zero, CoxeterSystem.getElem_leftInvSeq, OfNat.ofNat, Matrix.zero, one_mul, CoxeterSystem.alternatingWord_succ
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
rcases : ∀ (ω : List B), ∃ (n : ℕ) (ω_1 : List B), n = ω_1.length ∧ cs.wordProd ω_1 = cs.wordProd ω
⊢ ∃ (n : ℕ) (ω : List B), n = ω.length ∧ cs.wordProd ω = w

Tactic:
rcases cs.wordProd_surjective w with ⟨ω, rfl⟩

Premises used: CoxeterSystem.wordProd_surjective, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
w : ℕ
w₁ : List B
h : ω.length = ω.length ∧ cs.wordProd ω = cs.wordProd ω
⊢ ∃ (n : ℕ) (ω_1 : List B), n = ω_1.length ∧ cs.wordProd ω_1 = cs.wordProd ω

Tactic:
use ω.length, ω

Premises used: List.length
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
⊢ cs.length (cs.wordProd ω) = ω.length

Tactic:
hω

Premises used: CoxeterSystem.IsReduced
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
obtain :
  ∀ (ω : List B)
    (hω :
      Nat.find (p := fun (n : ℕ) ↦ ∃ (ω_1 : List B), n = ω_1.length ∧ cs.wordProd ω_1 = cs.wordProd ω) ⋯ = ω.length),
    ∃ (ω_1 : List B), cs.IsReduced ω_1 ∧ cs.wordProd ω = cs.wordProd ω_1
⊢ ∃ (ω : List B), cs.IsReduced ω ∧ w = cs.wordProd ω

Tactic:
obtain ⟨ω, hω, rfl⟩ := Nat.find_spec (cs.exists_word_with_prod w)

Premises used: _private.0.CoxeterSystem.exists_word_with_prod, rfl, Nat.find_spec
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : Nat.find (p := fun (n : ℕ) ↦ ∃ (ω_1 : List B), n = ω_1.length ∧ cs.wordProd ω_1 = cs.wordProd ω) ⋯ = ω.length
⊢ ∃ (ω_1 : List B), cs.IsReduced ω_1 ∧ cs.wordProd ω = cs.wordProd ω_1

Tactic:
⟨ω, hω, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : Nat.find (p := fun (n : ℕ) ↦ ∃ (ω_1 : List B), n = ω_1.length ∧ cs.wordProd ω_1 = cs.wordProd ω) ⋯ = ω.length
⊢ ∃ (ω_1 : List B), cs.IsReduced ω_1 ∧ cs.wordProd ω = cs.wordProd ω_1

Tactic:
exact ⟨ω, hω, rfl⟩
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
obtain :
  ∀ (ω : List B)
    (hω :
      Nat.find (p := fun (n : ℕ) ↦ ∃ (ω_1 : List B), n = ω_1.length ∧ cs.wordProd ω_1 = cs.wordProd ω) ⋯ = ω.length),
    ∃ (ω_1 : List B), cs.IsReduced ω_1 ∧ cs.wordProd ω = cs.wordProd ω_1
⊢ ∃ (ω : List B), cs.IsReduced ω ∧ w = cs.wordProd ω

Tactic:
classical
  obtain ⟨ω, hω, rfl⟩ := Nat.find_spec (cs.exists_word_with_prod w)
  exact ⟨ω, hω, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ cs.length (cs.wordProd ω) ≤ ω.length

Tactic:
Nat.find_min' (cs.exists_word_with_prod (π ω)) ⟨ω, rfl, rfl⟩

Premises used: _private.0.CoxeterSystem.exists_word_with_prod, CoxeterSystem.length, Nat.find_min', And.intro, Exists.intro, CoxeterSystem.wordProd, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ cs.length 1 = 0

Tactic:
Nat.eq_zero_of_le_zero (cs.length_wordProd_le [])

Premises used: CoxeterSystem.length_wordProd_le, Nat.eq_zero_of_le_zero, List.nil
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
mp : cs.length w = 0 → w = 1
mpr : w = 1 → cs.length w = 0
⊢ cs.length w = 0 ↔ w = 1

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
h : cs.length w = 0
mp : ∀ (ω : List B) (hω : cs.IsReduced ω) (h : cs.length (cs.wordProd ω) = 0), cs.wordProd ω = 1
⊢ w = 1

Tactic:
rcases cs.exists_isReduced w with ⟨ω, hω, rfl⟩

Premises used: CoxeterSystem.exists_isReduced, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
h : cs.length (cs.wordProd ω) = 0
⊢ ω = []

Tactic:
have : ω = [] := eq_nil_of_length_eq_zero (hω.symm.trans h)
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
h : cs.length (cs.wordProd ω) = 0
this : ω = []
mp : cs.wordProd [] = 1
mp₁ mp₂ : Eq.{u_2 + 1} (α := W) 1 1
⊢ cs.wordProd ω = 1

Tactic:
rw [this, wordProd_nil]

Premises used: CoxeterSystem.wordProd_nil
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ cs.length 1 = 0

Tactic:
cs.length_one

Premises used: CoxeterSystem.length_one
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ cs.length 1 = 0

Tactic:
exact cs.length_one

Premises used: CoxeterSystem.length_one
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
h₁ : cs.length w⁻¹ ≤ cs.length w
h₂ : cs.length w ≤ cs.length w⁻¹
⊢ cs.length w⁻¹ = cs.length w

Tactic:
apply Nat.le_antisymm

Premises used: Nat.le_antisymm
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
h₁ : ∀ (ω : List B) (hω : cs.IsReduced ω), cs.length (cs.wordProd ω)⁻¹ ≤ cs.length (cs.wordProd ω)
⊢ cs.length w⁻¹ ≤ cs.length w

Tactic:
rcases cs.exists_isReduced w with ⟨ω, hω, rfl⟩

Premises used: CoxeterSystem.exists_isReduced, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
⊢ cs.length (cs.wordProd ω.reverse) ≤ ω.reverse.length

Tactic:
have := cs.length_wordProd_le ω.reverse
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
this : cs.length (cs.wordProd ω.reverse) ≤ ω.reverse.length
h₁ : ∀ (this : cs.length (cs.wordProd ω)⁻¹ ≤ ω.reverse.length), cs.length (cs.wordProd ω)⁻¹ ≤ cs.length (cs.wordProd ω)
h₂ : ∀ (this : cs.length (cs.wordProd ω)⁻¹ ≤ ω.length), cs.length (cs.wordProd ω)⁻¹ ≤ cs.length (cs.wordProd ω)
h₃ h₄ h₅ h₆ :
  ∀ (this : cs.length (cs.wordProd ω)⁻¹ ≤ cs.length (cs.wordProd ω)),
    cs.length (cs.wordProd ω)⁻¹ ≤ cs.length (cs.wordProd ω)
⊢ cs.length (cs.wordProd ω)⁻¹ ≤ cs.length (cs.wordProd ω)

Tactic:
rwa [wordProd_reverse, length_reverse, ← hω] at this

Premises used: CoxeterSystem.wordProd_reverse, List.length_reverse
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
h₂ : ∀ (ω : List B) (hω : cs.IsReduced ω) (h'ω : w⁻¹ = cs.wordProd ω), cs.length w ≤ cs.length w⁻¹
⊢ cs.length w ≤ cs.length w⁻¹

Tactic:
rcases cs.exists_isReduced w⁻¹ with ⟨ω, hω, h'ω⟩

Premises used: CoxeterSystem.exists_isReduced, Inv.inv
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
ω : List B
hω : cs.IsReduced ω
h'ω : w⁻¹ = cs.wordProd ω
⊢ cs.length (cs.wordProd ω.reverse) ≤ ω.reverse.length

Tactic:
have := cs.length_wordProd_le ω.reverse
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
ω : List B
hω : cs.IsReduced ω
h'ω : w⁻¹ = cs.wordProd ω
this : cs.length (cs.wordProd ω.reverse) ≤ ω.reverse.length
h₂ : ∀ (this : cs.length (cs.wordProd ω)⁻¹ ≤ ω.reverse.length), cs.length w ≤ cs.length w⁻¹
h₃ : ∀ (this : cs.length (cs.wordProd ω)⁻¹ ≤ ω.length), cs.length w ≤ cs.length w⁻¹
h₄ : ∀ (this : cs.length w⁻¹⁻¹ ≤ ω.length), cs.length w ≤ cs.length w⁻¹
h₅ : ∀ (this : cs.length w⁻¹⁻¹ ≤ cs.length (cs.wordProd ω)), cs.length w ≤ cs.length w⁻¹
h₆ : ∀ (this : cs.length w ≤ cs.length (cs.wordProd ω)), cs.length w ≤ cs.length w⁻¹
h₇ h₈ h₉ h₁₀ : ∀ (this : cs.length w ≤ cs.length w⁻¹), cs.length w ≤ cs.length w⁻¹
⊢ cs.length w ≤ cs.length w⁻¹

Tactic:
rwa [wordProd_reverse, length_reverse, ← h'ω, ← hω, inv_inv, ← h'ω] at this

Premises used: CoxeterSystem.wordProd_reverse, List.length_reverse, inv_inv
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
rcases :
  ∀ (ω₁ : List B) (hω₁ : cs.IsReduced ω₁), cs.length (cs.wordProd ω₁ * w₂) ≤ cs.length (cs.wordProd ω₁) + cs.length w₂
⊢ cs.length (w₁ * w₂) ≤ cs.length w₁ + cs.length w₂

Tactic:
rcases cs.exists_isReduced w₁ with ⟨ω₁, hω₁, rfl⟩

Premises used: CoxeterSystem.exists_isReduced, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₂ : W
ω₁ : List B
hω₁ : cs.IsReduced ω₁
rcases :
  ∀ (ω₂ : List B) (hω₂ : cs.IsReduced ω₂),
    cs.length (cs.wordProd ω₁ * cs.wordProd ω₂) ≤ cs.length (cs.wordProd ω₁) + cs.length (cs.wordProd ω₂)
⊢ cs.length (cs.wordProd ω₁ * w₂) ≤ cs.length (cs.wordProd ω₁) + cs.length w₂

Tactic:
rcases cs.exists_isReduced w₂ with ⟨ω₂, hω₂, rfl⟩

Premises used: CoxeterSystem.exists_isReduced, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω₁ : List B
hω₁ : cs.IsReduced ω₁
ω₂ : List B
hω₂ : cs.IsReduced ω₂
⊢ cs.length (cs.wordProd (ω₁ ++ ω₂)) ≤ (ω₁ ++ ω₂).length

Tactic:
have := cs.length_wordProd_le (ω₁ ++ ω₂)
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω₁ : List B
hω₁ : cs.IsReduced ω₁
ω₂ : List B
hω₂ : cs.IsReduced ω₂
this : cs.length (cs.wordProd (ω₁ ++ ω₂)) ≤ (ω₁ ++ ω₂).length
⊢ cs.length (cs.wordProd ω₁ * cs.wordProd ω₂) ≤ cs.length (cs.wordProd ω₁) + cs.length (cs.wordProd ω₂)

Tactic:
simpa [hω₁.eq, hω₂.eq, wordProd_append] using this

Premises used: CoxeterSystem.IsReduced.eq, CoxeterSystem.wordProd_append
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length w₂ ≤ cs.length (w₁ * w₂) + cs.length w₁

Tactic:
simpa [add_comm] using cs.length_mul_le w₁⁻¹ (w₁ * w₂)

Premises used: HMul.hMul, CoxeterSystem.length_mul_le, add_comm, Inv.inv
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length w₁ ≤ cs.length (w₁ * w₂) + cs.length w₂

Tactic:
simpa using cs.length_mul_le (w₁ * w₂) w₂⁻¹

Premises used: HMul.hMul, CoxeterSystem.length_mul_le, Inv.inv
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
rw : cs.length w₁ ≤ cs.length (w₁ * w₂) + cs.length w₂
⊢ cs.length w₁ - cs.length w₂ ≤ cs.length (w₁ * w₂)

Tactic:
rw [Nat.sub_le_iff_le_add]

Premises used: Nat.sub_le_iff_le_add
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length w₁ ≤ cs.length (w₁ * w₂) + cs.length w₂

Tactic:
length_le_length_mul_add_right ..

Premises used: CoxeterSystem.length_le_length_mul_add_right
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length w₁ ≤ cs.length (w₁ * w₂) + cs.length w₂

Tactic:
exact length_le_length_mul_add_right ..

Premises used: CoxeterSystem.length_le_length_mul_add_right
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
rw : cs.length w₂ ≤ cs.length (w₁ * w₂) + cs.length w₁
⊢ cs.length w₂ - cs.length w₁ ≤ cs.length (w₁ * w₂)

Tactic:
rw [Nat.sub_le_iff_le_add]

Premises used: Nat.sub_le_iff_le_add
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length w₂ ≤ cs.length (w₁ * w₂) + cs.length w₁

Tactic:
length_le_length_mul_add_left ..

Premises used: CoxeterSystem.length_le_length_mul_add_left
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length w₂ ≤ cs.length (w₁ * w₂) + cs.length w₁

Tactic:
exact length_le_length_mul_add_left ..

Premises used: CoxeterSystem.length_le_length_mul_add_left
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ max (cs.length w₁ - cs.length w₂) (cs.length w₂ - cs.length w₁) ≤ cs.length (w₁ * w₂)

Tactic:
max_le (length_mul_ge_length_sub_length ..) (length_mul_ge_length_sub_length' ..)

Premises used: CoxeterSystem.length_mul_ge_length_sub_length', max_le, CoxeterSystem.length_mul_ge_length_sub_length
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ HAdd.hAdd (α := ZMod 2) 1 1 = 0

Tactic:
decide
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
simp_rw :
  ∀ (i i' : B),
    HPow.hPow (α := Multiplicative (ZMod 2)) ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 0)
        (M.M i i') =
      1
⊢ M.IsLiftable (G := Multiplicative (ZMod 2)) fun (x : B) ↦
    (Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 1

Tactic:
simp_rw [CoxeterMatrix.IsLiftable, ← ofAdd_add, (by decide : (1 + 1 : ZMod 2) = 0)]

Premises used: ofAdd_add, CoxeterMatrix.IsLiftable
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ ∀ (i i' : B),
    HPow.hPow (α := Multiplicative (ZMod 2)) ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 0)
        (M.M i i') =
      1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ Eq (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (cs.simple i) : Multiplicative (ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 1 : Multiplicative (ZMod 2))

Tactic:
cs.lift_apply_simple _ _

Premises used: CoxeterSystem.lift_apply_simple
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ Eq (α := B → Multiplicative (ZMod 2)) ((⇑cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) ∘ cs.simple)
    fun (x : B) ↦ (Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 1

Tactic:
funext cs.lengthParity_simple

Premises used: funext, CoxeterSystem.lengthParity_simple
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
rcases :
  ∀ (ω : List B) (hω : cs.IsReduced ω),
    Eq (α := Multiplicative (ZMod 2))
      ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (cs.wordProd ω) : Multiplicative (ZMod 2))
      ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑(cs.length (cs.wordProd ω)) : ZMod 2) :
        Multiplicative (ZMod 2))
⊢ Eq (α := Multiplicative (ZMod 2)) ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) w : Multiplicative (ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑(cs.length w) : ZMod 2) :
      Multiplicative (ZMod 2))

Tactic:
rcases cs.exists_isReduced w with ⟨ω, hω, rfl⟩

Premises used: CoxeterSystem.exists_isReduced, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
rw :
  Eq (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (cs.wordProd ω) : Multiplicative (ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑ω.length : ZMod 2) : Multiplicative (ZMod 2))
rw₁ :
  Eq (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (List.map cs.simple ω).prod : Multiplicative (ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑ω.length : ZMod 2) : Multiplicative (ZMod 2))
rw₂ :
  Eq (α := Multiplicative (ZMod 2))
    (prod (List.map (⇑cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (List.map cs.simple ω)))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑ω.length : ZMod 2))
rw₃ :
  Eq (α := Multiplicative (ZMod 2))
    (prod (List.map ((⇑cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) ∘ cs.simple) ω))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑ω.length : ZMod 2))
rw₄ :
  Eq (α := Multiplicative (ZMod 2))
    (prod (List.map (fun (x : B) ↦ (Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 1) ω))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑ω.length : ZMod 2))
rw₅ :
  Eq (α := Multiplicative (ZMod 2))
    (prod (replicate ω.length ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 1)))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑ω.length : ZMod 2))
rw₆ :
  HPow.hPow (α := Multiplicative (ZMod 2)) ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 1)
      ω.length =
    (Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑ω.length : ZMod 2)
rw₇ :
  Eq (α := Multiplicative (ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (HSMul.hSMul (β := ZMod 2) ω.length 1) :
      Multiplicative (ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑ω.length : ZMod 2) : Multiplicative (ZMod 2))
rw₈ rw₉ :
  Eq (α := Multiplicative (ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑ω.length : ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑ω.length : ZMod 2))
⊢ Eq (α := Multiplicative (ZMod 2))
    ((cs.lengthParity : (a : W) → Multiplicative (ZMod 2)) (cs.wordProd ω) : Multiplicative (ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑(cs.length (cs.wordProd ω)) : ZMod 2) :
      Multiplicative (ZMod 2))

Tactic:
rw [hω, wordProd, map_list_prod, List.map_map, lengthParity_comp_simple, map_const',
    prod_replicate, ← ofAdd_nsmul, nsmul_one]

Premises used: List.map_const', List.map_map, map_list_prod, CoxeterSystem.lengthParity_comp_simple, ofAdd_nsmul, CoxeterSystem.wordProd, nsmul_one, List.prod_replicate
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
rw : (↑(cs.length (w₁ * w₂)) : ZMod 2) = HAdd.hAdd (α := ZMod 2) (↑(cs.length w₁) : ZMod 2) (↑(cs.length w₂) : ZMod 2)
⊢ cs.length (w₁ * w₂) % 2 = (cs.length w₁ + cs.length w₂) % 2

Tactic:
rw [← ZMod.natCast_eq_natCast_iff', Nat.cast_add]

Premises used: ZMod.natCast_eq_natCast_iff', Nat.cast_add
-- Module: Mathlib.GroupTheory.Coxeter.Length
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ (↑(cs.length (w₁ * w₂)) : ZMod 2) = HAdd.hAdd (α := ZMod 2) (↑(cs.length w₁) : ZMod 2) (↑(cs.length w₂) : ZMod 2)

Tactic:
simpa only [lengthParity_eq_ofAdd_length, ofAdd_add] using map_mul cs.lengthParity w₁ w₂

Premises used: ofAdd_add, map_mul, CoxeterSystem.lengthParity, CoxeterSystem.lengthParity_eq_ofAdd_length