awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ ∃ (ω : List B), cs.IsReduced ω ∧ w = cs.wordProd ω
have obtain : ∀ (ω : List B)
  (hω : Nat.find (p := fun (n : ℕ) ↦ ∃ (ω_1 : List B), n = ω_1.length ∧ cs.wordProd ω_1 = cs.wordProd ω) sorry = ω.length),
  ∃ (ω_1 : List B), cs.IsReduced ω_1 ∧ cs.wordProd ω = cs.wordProd ω_1
Tactic: classical
  obtain ⟨ω, hω, rfl⟩ := Nat.find_spec (cs.exists_word_with_prod w)
  exact ⟨ω, hω, rfl⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.length w = 0 ↔ w = 1
have mp : cs.length w = 0 → w = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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
⊢ cs.length w = 0 ↔ w = 1
have mpr : w = 1 → cs.length w = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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
⊢ w = 1
have mp : ∀ (ω : List B) (hω : cs.IsReduced ω) (h : cs.length (cs.wordProd ω) = 0), cs.wordProd ω = 1
Tactic: rcases cs.exists_isReduced w with ⟨ω, hω, rfl⟩
Cleared hypotheses: w, h
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (hypothesis)
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
⊢ cs.wordProd ω = 1
have this : ω = []
Tactic: have : ω = [] := eq_nil_of_length_eq_zero (hω.symm.trans h)
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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 : ω = []
⊢ cs.wordProd ω = 1
have mp : cs.wordProd [] = 1
Tactic: rw [this, wordProd_nil]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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
⊢ cs.wordProd ω = 1
have mp₁ : Eq.{u_2 + 1} (α := W) 1 1
Tactic: rw [this, wordProd_nil]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.length w⁻¹ = cs.length w
have h₁ : cs.length w⁻¹ ≤ cs.length w
Tactic: apply Nat.le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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
⊢ cs.length w⁻¹ = cs.length w
have h₂ : cs.length w ≤ cs.length w⁻¹
Tactic: apply Nat.le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.length w⁻¹ ≤ cs.length w
have h₁ : ∀ (ω : List B) (hω : cs.IsReduced ω), cs.length (cs.wordProd ω)⁻¹ ≤ cs.length (cs.wordProd ω)
Tactic: rcases cs.exists_isReduced w with ⟨ω, hω, rfl⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (hypothesis)
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 ω)⁻¹ ≤ cs.length (cs.wordProd ω)
have this : cs.length (cs.wordProd ω.reverse) ≤ ω.reverse.length
Tactic: have := cs.length_wordProd_le ω.reverse
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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
⊢ cs.length (cs.wordProd ω)⁻¹ ≤ cs.length (cs.wordProd ω)
have h₁ : ∀ (this : cs.length (cs.wordProd ω)⁻¹ ≤ ω.reverse.length), cs.length (cs.wordProd ω)⁻¹ ≤ cs.length (cs.wordProd ω)
Tactic: rwa [wordProd_reverse, length_reverse, ← hω] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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 ω)
⊢ cs.length (cs.wordProd ω)⁻¹ ≤ cs.length (cs.wordProd ω)
have h₂ : ∀ (this : cs.length (cs.wordProd ω)⁻¹ ≤ ω.length), cs.length (cs.wordProd ω)⁻¹ ≤ cs.length (cs.wordProd ω)
Tactic: rwa [wordProd_reverse, length_reverse, ← hω] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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 ω)
⊢ cs.length (cs.wordProd ω)⁻¹ ≤ cs.length (cs.wordProd ω)
have h₃ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.length w ≤ cs.length w⁻¹
have h₂ : ∀ (ω : List B) (hω : cs.IsReduced ω) (h'ω : w⁻¹ = cs.wordProd ω), cs.length w ≤ cs.length w⁻¹
Tactic: rcases cs.exists_isReduced w⁻¹ with ⟨ω, hω, h'ω⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (hypothesis)
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 w ≤ cs.length w⁻¹
have this : cs.length (cs.wordProd ω.reverse) ≤ ω.reverse.length
Tactic: have := cs.length_wordProd_le ω.reverse
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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
⊢ cs.length w ≤ cs.length w⁻¹
have h₂ : ∀ (this : cs.length (cs.wordProd ω)⁻¹ ≤ ω.reverse.length), cs.length w ≤ cs.length w⁻¹
Tactic: rwa [wordProd_reverse, length_reverse, ← h'ω, ← hω, inv_inv, ← h'ω] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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⁻¹
⊢ cs.length w ≤ cs.length w⁻¹
have h₃ : ∀ (this : cs.length (cs.wordProd ω)⁻¹ ≤ ω.length), cs.length w ≤ cs.length w⁻¹
Tactic: rwa [wordProd_reverse, length_reverse, ← h'ω, ← hω, inv_inv, ← h'ω] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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⁻¹
⊢ cs.length w ≤ cs.length w⁻¹
have h₄ : ∀ (this : cs.length w⁻¹⁻¹ ≤ ω.length), cs.length w ≤ cs.length w⁻¹
Tactic: rwa [wordProd_reverse, length_reverse, ← h'ω, ← hω, inv_inv, ← h'ω] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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⁻¹
⊢ cs.length w ≤ cs.length w⁻¹
have h₅ : ∀ (this : cs.length w⁻¹⁻¹ ≤ cs.length (cs.wordProd ω)), cs.length w ≤ cs.length w⁻¹
Tactic: rwa [wordProd_reverse, length_reverse, ← h'ω, ← hω, inv_inv, ← h'ω] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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⁻¹
⊢ cs.length w ≤ cs.length w⁻¹
have h₆ : ∀ (this : cs.length w ≤ cs.length (cs.wordProd ω)), cs.length w ≤ cs.length w⁻¹
Tactic: rwa [wordProd_reverse, length_reverse, ← h'ω, ← hω, inv_inv, ← h'ω] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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⁻¹
⊢ cs.length w ≤ cs.length w⁻¹
have h₇ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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₂) ≤ cs.length w₁ + cs.length w₂
have rcases : ∀ (ω₁ : List B) (hω₁ : cs.IsReduced ω₁), cs.length (cs.wordProd ω₁ * w₂) ≤ cs.length (cs.wordProd ω₁) + cs.length w₂
Tactic: rcases cs.exists_isReduced w₁ with ⟨ω₁, hω₁, rfl⟩
Cleared hypotheses: w₁
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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 ω₁
⊢ cs.length (cs.wordProd ω₁ * w₂) ≤ cs.length (cs.wordProd ω₁) + cs.length w₂
have rcases : ∀ (ω₂ : List B) (hω₂ : cs.IsReduced ω₂),
  cs.length (cs.wordProd ω₁ * cs.wordProd ω₂) ≤ cs.length (cs.wordProd ω₁) + cs.length (cs.wordProd ω₂)
Tactic: rcases cs.exists_isReduced w₂ with ⟨ω₂, hω₂, rfl⟩
Cleared hypotheses: w₂
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (hypothesis)
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 ω₁ * cs.wordProd ω₂) ≤ cs.length (cs.wordProd ω₁) + cs.length (cs.wordProd ω₂)
have this : cs.length (cs.wordProd (ω₁ ++ ω₂)) ≤ (ω₁ ++ ω₂).length
Tactic: have := cs.length_wordProd_le (ω₁ ++ ω₂)
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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₂ ≤ cs.length (w₁ * w₂)
have rw : cs.length w₁ ≤ cs.length (w₁ * w₂) + cs.length w₂
Tactic: rw [Nat.sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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₁ ≤ cs.length (w₁ * w₂)
have rw : cs.length w₂ ≤ cs.length (w₁ * w₂) + cs.length w₁
Tactic: rw [Nat.sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ M.IsLiftable (G := Multiplicative (ZMod 2)) fun (x : B) ↦
    (Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 1
have simp_rw : ∀ (i i' : B),
  HPow.hPow (α := Multiplicative (ZMod 2)) ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 0)
      (M.M i i') =
    1
Tactic: simp_rw [CoxeterMatrix.IsLiftable, ← ofAdd_add, (by decide : (1 + 1 : ZMod 2) = 0)]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ 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))
have 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))
Tactic: rcases cs.exists_isReduced w with ⟨ω, hω, rfl⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : 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))
have 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))
Tactic: rw [hω, wordProd, map_list_prod, List.map_map, lengthParity_comp_simple, map_const',
    prod_replicate, ← ofAdd_nsmul, nsmul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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))
⊢ 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))
have 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))
Tactic: rw [hω, wordProd, map_list_prod, List.map_map, lengthParity_comp_simple, map_const',
    prod_replicate, ← ofAdd_nsmul, nsmul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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))
⊢ 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))
have 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))
Tactic: rw [hω, wordProd, map_list_prod, List.map_map, lengthParity_comp_simple, map_const',
    prod_replicate, ← ofAdd_nsmul, nsmul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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))
⊢ 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))
have 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))
Tactic: rw [hω, wordProd, map_list_prod, List.map_map, lengthParity_comp_simple, map_const',
    prod_replicate, ← ofAdd_nsmul, nsmul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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))
⊢ 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))
have 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))
Tactic: rw [hω, wordProd, map_list_prod, List.map_map, lengthParity_comp_simple, map_const',
    prod_replicate, ← ofAdd_nsmul, nsmul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
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))
⊢ 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))
have 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))
Tactic: rw [hω, wordProd, map_list_prod, List.map_map, lengthParity_comp_simple, map_const',
    prod_replicate, ← ofAdd_nsmul, nsmul_one]