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
ω : 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))
⊢ 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₆ : 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)
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))
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)
⊢ 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))
  ((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))
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))
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))
⊢ 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)) ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑ω.length : ZMod 2))
  ((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
w₁ w₂ : W
⊢ cs.length (w₁ * w₂) % 2 = (cs.length w₁ + cs.length w₂) % 2
have rw : (↑(cs.length (w₁ * w₂)) : ZMod 2) = HAdd.hAdd (α := ZMod 2) (↑(cs.length w₁) : ZMod 2) (↑(cs.length w₂) : ZMod 2)
Tactic: rw [← ZMod.natCast_eq_natCast_iff', Nat.cast_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
i : B
⊢ cs.length (cs.simple i) = 1
have h₁ : cs.length (cs.simple i) ≤ 1
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
i : B
h₁ : cs.length (cs.simple i) ≤ 1
⊢ cs.length (cs.simple i) = 1
have h₂ : 1 ≤ cs.length (cs.simple i)
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
i : B
⊢ 1 ≤ cs.length (cs.simple i)
have h₂ : ∀ (length_lt_one : cs.length (cs.simple i) < 1), False
Tactic: by_contra! length_lt_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
i : B
length_lt_one : cs.length (cs.simple i) < 1
⊢ 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)) 0 : Multiplicative (ZMod 2))
have rw : Eq (α := Multiplicative (ZMod 2))
  ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑(cs.length (cs.simple i)) : ZMod 2))
  ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 0)
Tactic: rw [lengthParity_eq_ofAdd_length, Nat.lt_one_iff.mp length_lt_one, Nat.cast_zero]
-- 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
i : B
length_lt_one : cs.length (cs.simple i) < 1
rw :
  Eq (α := Multiplicative (ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑(cs.length (cs.simple i)) : ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 0)
⊢ 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)) 0 : Multiplicative (ZMod 2))
have rw₁ : Eq (α := Multiplicative (ZMod 2)) ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑0 : ZMod 2))
  ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 0)
Tactic: rw [lengthParity_eq_ofAdd_length, Nat.lt_one_iff.mp length_lt_one, Nat.cast_zero]
-- 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
i : B
length_lt_one : cs.length (cs.simple i) < 1
rw :
  Eq (α := Multiplicative (ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑(cs.length (cs.simple i)) : ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 0)
rw₁ :
  Eq (α := Multiplicative (ZMod 2)) ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) (↑0 : ZMod 2))
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 0)
⊢ 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)) 0 : Multiplicative (ZMod 2))
have rw₂ : Eq (α := Multiplicative (ZMod 2)) ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 0)
  ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 0)
Tactic: rw [lengthParity_eq_ofAdd_length, Nat.lt_one_iff.mp length_lt_one, Nat.cast_zero]
-- 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
i : B
length_lt_one : cs.length (cs.simple i) < 1
⊢ False
have this : 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)) 0 : Multiplicative (ZMod 2))
Tactic: have : cs.lengthParity (s i) = Multiplicative.ofAdd 0 := by
      rw [lengthParity_eq_ofAdd_length, Nat.lt_one_iff.mp length_lt_one, Nat.cast_zero]
-- 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
i : B
length_lt_one : cs.length (cs.simple i) < 1
this :
  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)) 0 : Multiplicative (ZMod 2))
⊢ False
have this₁ : Eq (α := Multiplicative (ZMod 2)) ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 0)
  ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 1)
Tactic: have : Multiplicative.ofAdd (0 : ZMod 2) = Multiplicative.ofAdd 1 :=
      this.symm.trans (cs.lengthParity_simple i)
-- 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 = 1 ↔ ∃ (i : B), w = cs.simple i
have mp : cs.length w = 1 → ∃ (i : B), w = cs.simple i
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 = 1 → ∃ (i : B), w = cs.simple i
⊢ cs.length w = 1 ↔ ∃ (i : B), w = cs.simple i
have mpr : (∃ (i : B), w = cs.simple i) → cs.length 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
h : cs.length w = 1
⊢ ∃ (i : B), w = cs.simple i
have mp : ∀ (ω : List B) (hω : cs.IsReduced ω) (h : cs.length (cs.wordProd ω) = 1), ∃ (i : B), cs.wordProd ω = cs.simple i
Tactic: rcases cs.exists_isReduced w with ⟨ω, hω, rfl⟩
Cleared hypotheses: w, 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 ω) = 1
⊢ ∃ (i : B), cs.wordProd ω = cs.simple i
have mp : ∀ (i : B) (hω : cs.IsReduced [i]) (h : cs.length (cs.wordProd [i]) = 1), ∃ (i_1 : B), cs.wordProd [i] = cs.simple i_1
Tactic: rcases List.length_eq_one_iff.mp (hω.symm.trans h) with ⟨i, rfl⟩
Cleared hypotheses: ω, 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
i : B
eq : cs.length (w * cs.simple i) = cs.length w
⊢ False
have length_mod_two : cs.length (w * cs.simple i) % 2 = (cs.length w + cs.length (cs.simple i)) % 2
Tactic: have length_mod_two := cs.length_mul_mod_two w (s i)
-- 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
i : B
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : cs.length (w * cs.simple i) % 2 = (cs.length w + cs.length (cs.simple i)) % 2
⊢ False
have length_mod_two₁ : cs.length w % 2 = (cs.length w + 1) % 2
Tactic: rw [eq, length_simple] at length_mod_two
Cleared hypotheses: length_mod_two
-- 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
i : B
⊢ cs.length (cs.simple i * w) ≠ cs.length w
have rw : cs.length (cs.simple i * w)⁻¹ ≠ cs.length w
Tactic: rw [← length_inv]
-- 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
i : B
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
have inl : ∀ (h : cs.length (w * cs.simple i) < cs.length w),
  cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
Tactic: rcases (cs.length_mul_simple_ne w i).lt_or_gt with h | 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
w : W
i : B
inl :
  ∀ (h : cs.length (w * cs.simple i) < cs.length w),
    cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
have inr : ∀ (h : cs.length w < cs.length (w * cs.simple i)),
  cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
Tactic: rcases (cs.length_mul_simple_ne w i).lt_or_gt 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
i : B
h : cs.length (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
have h₁ : cs.length (w * cs.simple i) + 1 ≤ cs.length w
Tactic: rw [← Nat.add_one_le_iff] at h
Cleared hypotheses: 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
i : B
h : cs.length w < cs.length (w * cs.simple i)
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
have h₁ : cs.length w + 1 ≤ cs.length (w * cs.simple i)
Tactic: rw [← Nat.add_one_le_iff] at h
Cleared hypotheses: 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
w : W
i : B
h : cs.length (w * cs.simple i) + 1 ≤ cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
have inl : cs.length w ≤ cs.length (w * cs.simple i) + 1
Tactic: refine .inr (h.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
i : B
h : cs.length w + 1 ≤ cs.length (w * cs.simple i)
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
have inr : cs.length (w * cs.simple i) ≤ cs.length w + 1
Tactic: refine .inl (h.antisymm' ?_)
-- 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
i : B
⊢ cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
have this : cs.length (w⁻¹ * cs.simple i) = cs.length w⁻¹ + 1 ∨ cs.length (w⁻¹ * cs.simple i) + 1 = cs.length w⁻¹
Tactic: have := cs.length_mul_simple w⁻¹ i
-- 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
i : B
this : cs.length (w⁻¹ * cs.simple i) = cs.length w⁻¹ + 1 ∨ cs.length (w⁻¹ * cs.simple i) + 1 = cs.length w⁻¹
⊢ cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
have rwa : w⁻¹ * cs.simple i = (cs.simple i * w)⁻¹
Tactic: rwa [(by simp : w⁻¹ * (s i) = ((s i) * w)⁻¹), length_inv, length_inv] at 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
i : B
this : cs.length (w⁻¹ * cs.simple i) = cs.length w⁻¹ + 1 ∨ cs.length (w⁻¹ * cs.simple i) + 1 = cs.length w⁻¹
rwa : w⁻¹ * cs.simple i = (cs.simple i * w)⁻¹
⊢ cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
have rwa₁ : ∀ (this : cs.length (cs.simple i * w)⁻¹ = cs.length w⁻¹ + 1 ∨ cs.length (cs.simple i * w)⁻¹ + 1 = cs.length w⁻¹),
  cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
Tactic: rwa [(by simp : w⁻¹ * (s i) = ((s i) * w)⁻¹), length_inv, length_inv] 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
i : B
this : cs.length (w⁻¹ * cs.simple i) = cs.length w⁻¹ + 1 ∨ cs.length (w⁻¹ * cs.simple i) + 1 = cs.length w⁻¹
rwa : w⁻¹ * cs.simple i = (cs.simple i * w)⁻¹
rwa₁ :
  ∀ (this : cs.length (cs.simple i * w)⁻¹ = cs.length w⁻¹ + 1 ∨ cs.length (cs.simple i * w)⁻¹ + 1 = cs.length w⁻¹),
    cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
⊢ cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
have rwa₂ : ∀ (this : cs.length (cs.simple i * w) = cs.length w⁻¹ + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w⁻¹),
  cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
Tactic: rwa [(by simp : w⁻¹ * (s i) = ((s i) * w)⁻¹), length_inv, length_inv] 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
i : B
this : cs.length (w⁻¹ * cs.simple i) = cs.length w⁻¹ + 1 ∨ cs.length (w⁻¹ * cs.simple i) + 1 = cs.length w⁻¹
rwa : w⁻¹ * cs.simple i = (cs.simple i * w)⁻¹
rwa₁ :
  ∀ (this : cs.length (cs.simple i * w)⁻¹ = cs.length w⁻¹ + 1 ∨ cs.length (cs.simple i * w)⁻¹ + 1 = cs.length w⁻¹),
    cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
rwa₂ :
  ∀ (this : cs.length (cs.simple i * w) = cs.length w⁻¹ + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w⁻¹),
    cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
⊢ cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
have rwa₃ : ∀ (this : cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w),
  cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
Tactic: rwa [(by simp : w⁻¹ * (s i) = ((s i) * w)⁻¹), length_inv, length_inv] at this
Cleared hypotheses: this
-- 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 ω
j : ℕ
⊢ cs.IsReduced (take j ω) ∧ cs.IsReduced (drop j ω)
have h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
Tactic: have h₁ : ℓ (π (ω.take j)) ≤ (ω.take j).length := cs.length_wordProd_le (ω.take j)
-- 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 ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
⊢ cs.IsReduced (take j ω) ∧ cs.IsReduced (drop j ω)
have h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length
Tactic: have h₂ : ℓ (π (ω.drop j)) ≤ (ω.drop j).length := cs.length_wordProd_le (ω.drop j)
-- 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 ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length
⊢ (take j ω).length + (drop j ω).length = ω.length
have rw : (take j ω ++ drop j ω).length = ω.length
Tactic: rw [← List.length_append, ω.take_append_drop j]
-- 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 ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length
rw : (take j ω ++ drop j ω).length = ω.length
⊢ (take j ω).length + (drop j ω).length = ω.length
have rw₁ : ω.length = ω.length
Tactic: rw [← List.length_append, ω.take_append_drop j]