awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h₁ : cs.length (cs.simple i) ≤ 1
h₂ : 1 ≤ cs.length (cs.simple i)
⊢ cs.length (cs.simple i) = 1

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
i : B
⊢ cs.length (cs.simple i) ≤ 1

Tactic:
simpa using cs.length_wordProd_le [i]

Premises used: CoxeterSystem.length_wordProd_le, List.cons, 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
i : B
h₂ : ∀ (length_lt_one : cs.length (cs.simple i) < 1), False
⊢ 1 ≤ cs.length (cs.simple i)

Tactic:
by_contra! length_lt_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
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)
rw₂ rw₃ :
  Eq (α := Multiplicative (ZMod 2)) ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 0)
    ((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))

Tactic:
rw [lengthParity_eq_ofAdd_length, Nat.lt_one_iff.mp length_lt_one, Nat.cast_zero]

Premises used: Nat.lt_one_iff, Iff.mp, CoxeterSystem.lengthParity_eq_ofAdd_length, Nat.cast_zero
-- 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
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))

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]
-- 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
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))
⊢ 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)
-- 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
length_lt_one : cs.length (cs.simple i) < 1
this_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))
this :
  Eq (α := Multiplicative (ZMod 2)) ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 0)
    ((Multiplicative.ofAdd : (a : ZMod 2) → Multiplicative (ZMod 2)) 1)
⊢ False

Tactic:
contradiction
-- 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 = 1 → ∃ (i : B), w = cs.simple i
mpr : (∃ (i : B), w = cs.simple i) → cs.length w = 1
⊢ cs.length w = 1 ↔ ∃ (i : B), w = cs.simple i

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 = 1
mp : ∀ (ω : List B) (hω : cs.IsReduced ω) (h : cs.length (cs.wordProd ω) = 1), ∃ (i : B), cs.wordProd ω = cs.simple i
⊢ ∃ (i : B), w = cs.simple i

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 ω) = 1
mp :
  ∀ (i : B) (hω : cs.IsReduced [i]) (h : cs.length (cs.wordProd [i]) = 1), ∃ (i_1 : B), cs.wordProd [i] = cs.simple i_1
⊢ ∃ (i : B), cs.wordProd ω = cs.simple i

Tactic:
rcases List.length_eq_one_iff.mp (hω.symm.trans h) with ⟨i, rfl⟩

Premises used: List.length_eq_one_iff, Iff.mp, Eq.symm, rfl, Eq.trans
-- 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
hω : cs.IsReduced [i]
h : cs.length (cs.wordProd [i]) = 1
⊢ ∃ (i_1 : B), cs.wordProd [i] = cs.simple i_1

Tactic:
⟨i, cs.wordProd_singleton i⟩

Premises used: CoxeterSystem.wordProd_singleton, Exists.intro
-- 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
hω : cs.IsReduced [i]
h : cs.length (cs.wordProd [i]) = 1
⊢ ∃ (i_1 : B), cs.wordProd [i] = cs.simple i_1

Tactic:
exact ⟨i, cs.wordProd_singleton i⟩
-- 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
⊢ cs.length (cs.simple i) = 1

Tactic:
cs.length_simple i

Premises used: CoxeterSystem.length_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
i : B
⊢ cs.length (cs.simple i) = 1

Tactic:
exact cs.length_simple i

Premises used: CoxeterSystem.length_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
i : B
eq : cs.length (w * cs.simple i) = cs.length w
⊢ 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)
-- 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
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
⊢ cs.length w % 2 = (cs.length w + 1) % 2

Tactic:
rw [eq, length_simple] at length_mod_two

Premises used: CoxeterSystem.length_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
i : B
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : cs.length w % 2 = (cs.length w + 1) % 2
⊢ False

Tactic:
lia
-- 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
i : B
rw : cs.length (cs.simple i * w)⁻¹ ≠ cs.length w
⊢ cs.length (cs.simple i * w) ≠ cs.length w

Tactic:
rw [← length_inv]

Premises used: CoxeterSystem.length_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
i : B
⊢ cs.length (cs.simple i * w)⁻¹ ≠ cs.length w

Tactic:
simpa using cs.length_mul_simple_ne w⁻¹ i

Premises used: Inv.inv, CoxeterSystem.length_mul_simple_ne
-- 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
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
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
⊢ 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

Premises used: CoxeterSystem.length_mul_simple_ne, Ne.lt_or_gt
-- 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
i : B
h : cs.length (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) + 1 ≤ cs.length w

Tactic:
rw [← Nat.add_one_le_iff] at h

Premises used: Nat.add_one_le_iff
-- 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
i : B
h : cs.length w < cs.length (w * cs.simple i)
⊢ cs.length w + 1 ≤ cs.length (w * cs.simple i)

Tactic:
rw [← Nat.add_one_le_iff] at h

Premises used: Nat.add_one_le_iff
-- 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
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

Tactic:
.inr (h.antisymm ?_)

Premises used: LE.le.antisymm, Or.inr
-- 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
i : B
h : cs.length (w * cs.simple i) + 1 ≤ cs.length w
inl : cs.length w ≤ cs.length (w * cs.simple i) + 1
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
refine .inr (h.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
i : B
h : cs.length (w * cs.simple i) + 1 ≤ cs.length w
⊢ cs.length w ≤ cs.length (w * cs.simple i) + 1

Tactic:
simpa using cs.length_le_length_mul_add_right w (s i)
-- 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
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

Tactic:
.inl (h.antisymm' ?_)

Premises used: LE.le.antisymm', Or.inl
-- 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
i : B
h : cs.length w + 1 ≤ cs.length (w * cs.simple i)
inr : cs.length (w * cs.simple i) ≤ cs.length w + 1
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
refine .inl (h.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
i : B
h : cs.length w + 1 ≤ cs.length (w * cs.simple i)
⊢ cs.length (w * cs.simple i) ≤ cs.length w + 1

Tactic:
simpa using cs.length_mul_le w (s i)
-- 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
i : B
⊢ 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
-- 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
i : B
this : cs.length (w⁻¹ * cs.simple i) = cs.length w⁻¹ + 1 ∨ cs.length (w⁻¹ * cs.simple i) + 1 = cs.length w⁻¹
⊢ w⁻¹ * cs.simple i = (cs.simple i * w)⁻¹

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
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
rwa₃ rwa₄ rwa₅ 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

Tactic:
rwa [(by simp : w⁻¹ * (s i) = ((s i) * w)⁻¹), length_inv, length_inv] at this

Premises used: CoxeterSystem.length_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
ω : List B
⊢ cs.IsReduced ω.reverse ↔ cs.IsReduced ω

Tactic:
simp [IsReduced]

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
ω : List B
hω : cs.IsReduced ω
⊢ cs.IsReduced ω.reverse

Tactic:
(cs.isReduced_reverse_iff ω).mpr hω

Premises used: Iff.mpr, CoxeterSystem.isReduced_reverse_iff
-- 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 ω
j : ℕ
⊢ cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length

Tactic:
have h₁ : ℓ (π (ω.take j)) ≤ (ω.take j).length := cs.length_wordProd_le (ω.take j)
-- 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 ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
⊢ cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length

Tactic:
have h₂ : ℓ (π (ω.drop j)) ≤ (ω.drop j).length := cs.length_wordProd_le (ω.drop j)
-- 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 ω
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
rw₁ rw₂ : ω.length = ω.length
⊢ (take j ω).length + (drop j ω).length = ω.length

Tactic:
rw [← List.length_append, ω.take_append_drop j]

Premises used: List.take_append_drop, List.length_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
ω : 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 : cs.length (cs.wordProd ω) = cs.length (cs.wordProd (take j ω ++ drop j ω))
rw₁ rw₂ : cs.length (cs.wordProd ω) = cs.length (cs.wordProd ω)
⊢ cs.length (cs.wordProd ω) = cs.length (cs.wordProd (take j ω) * cs.wordProd (drop j ω))

Tactic:
rw [← cs.wordProd_append, ω.take_append_drop j]

Premises used: List.take_append_drop, 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
ω : 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 ≤ cs.length (cs.wordProd (take j ω)) + cs.length (cs.wordProd (drop j ω))

Tactic:
have h₃ := calc
    (ω.take j).length + (ω.drop j).length
    _ = ω.length := by rw [← List.length_append, ω.take_append_drop j]
    _ = ℓ (π ω) := hω.symm
    _ = ℓ (π (ω.take j) * π (ω.drop j)) := by rw [← cs.wordProd_append, ω.take_append_drop j]
    _ ≤ ℓ (π (ω.take j)) + ℓ (π (ω.drop j)) := cs.length_mul_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 ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length
h₃ : (take j ω).length + (drop j ω).length ≤ cs.length (cs.wordProd (take j ω)) + cs.length (cs.wordProd (drop j ω))
⊢ cs.length (cs.wordProd (take j ω)) = (take j ω).length ∧ cs.length (cs.wordProd (drop j ω)) = (drop j ω).length

Tactic:
lia
-- 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 ω
j : ℕ
⊢ cs.IsReduced (List.take j ω)

Tactic:
(isReduced_take_and_drop _ hω _).1

Premises used: And.left, _private.0.CoxeterSystem.isReduced_take_and_drop
-- 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 ω
j : ℕ
⊢ cs.IsReduced (List.drop j ω)

Tactic:
(isReduced_take_and_drop _ hω _).2

Premises used: And.right, _private.0.CoxeterSystem.isReduced_take_and_drop
-- 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
m : ℕ
hM : M.M i i' ≠ 0
h : cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
rw : ¬cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) = M.M i i' + 1
⊢ ¬cs.length (cs.wordProd (alternatingWord i i' (M.M i i').succ)) = (alternatingWord i i' (M.M i i').succ).length

Tactic:
rw [Nat.succ_eq_add_one, length_alternatingWord]

Premises used: Nat.succ_eq_add_one, CoxeterSystem.length_alternatingWord
-- 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
m : ℕ
hM : M.M i i' ≠ 0
h : cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
⊢ ¬cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) = M.M i i' + 1

Tactic:
lia
-- 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
m : ℕ
hM : M.M i i' ≠ 0
refl : cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
⊢ ¬cs.IsReduced (alternatingWord i i' (M.M i i').succ)

Tactic:
suffices h : ℓ (π (alternatingWord i i' (M i i' + 1))) < M i i' + 1 by
      unfold IsReduced
      rw [Nat.succ_eq_add_one, length_alternatingWord]
      lia
-- 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
m : ℕ
hM : M.M i i' ≠ 0
linarith :
  M.M i i' * 2 < M.M i i' + 1 →
    -1 + (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑(M.M i i') : ℤ) 1) +
        HSub.hSub (α := ℤ) 1 (↑(M.M i i') : ℤ) =
      0
⊢ M.M i i' + 1 ≤ M.M i i' * 2

Tactic:
linarith [Nat.one_le_iff_ne_zero.mpr hM]

Premises used: Iff.mpr, Nat.one_le_iff_ne_zero
-- 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
m : ℕ
hM : M.M i i' ≠ 0
⊢ M.M i i' + 1 ≤ M.M i i' * 2

Tactic:
have : M i i' + 1 ≤ M i i' * 2 := by linarith [Nat.one_le_iff_ne_zero.mpr hM]
-- 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
m : ℕ
hM : M.M i i' ≠ 0
this : M.M i i' + 1 ≤ M.M i i' * 2
refl : cs.length (cs.wordProd (alternatingWord i' i (M.M i i' * 2 - (M.M i i' + 1)))) < M.M i i' + 1
⊢ cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1

Tactic:
rw [cs.prod_alternatingWord_eq_prod_alternatingWord_sub i i' _ this]

Premises used: CoxeterSystem.prod_alternatingWord_eq_prod_alternatingWord_sub
-- 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
m : ℕ
hM : M.M i i' ≠ 0
this : M.M i i' + 1 ≤ M.M i i' * 2
⊢ M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1

Tactic:
lia
-- 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
m : ℕ
hM : M.M i i' ≠ 0
this : M.M i i' + 1 ≤ M.M i i' * 2
⊢ M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1

Tactic:
have : M i i' * 2 - (M i i' + 1) = M i i' - 1 := by lia
-- 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
m : ℕ
hM : M.M i i' ≠ 0
this_1 : M.M i i' + 1 ≤ M.M i i' * 2
this : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
refl : cs.length (cs.wordProd (alternatingWord i' i (M.M i i' - 1))) < M.M i i' + 1
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' * 2 - (M.M i i' + 1)))) < M.M i i' + 1

Tactic:
rw [this]
-- 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
m : ℕ
hM : M.M i i' ≠ 0
this_1 : M.M i i' + 1 ≤ M.M i i' * 2
this : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' - 1))) ≤ (alternatingWord i' i (M.M i i' - 1)).length

Tactic:
cs.length_wordProd_le _

Premises used: CoxeterSystem.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
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this_1 : M.M i i' + 1 ≤ M.M i i' * 2
this : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
⊢ (alternatingWord i' i (M.M i i' - 1)).length = M.M i i' - 1

Tactic:
length_alternatingWord _ _ _

Premises used: CoxeterSystem.length_alternatingWord
-- 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
m : ℕ
hM : M.M i i' ≠ 0
this_1 : M.M i i' + 1 ≤ M.M i i' * 2
this : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
⊢ M.M i i' - 1 ≤ M.M i i'

Tactic:
Nat.sub_le _ _

Premises used: Nat.sub_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
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this_1 : M.M i i' + 1 ≤ M.M i i' * 2
this : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
⊢ M.M i i' < M.M i i' + 1

Tactic:
Nat.lt_succ_self _

Premises used: Nat.lt_succ_self
-- 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
m : ℕ
hM : M.M i i' ≠ 0
this_1 : M.M i i' + 1 ≤ M.M i i' * 2
this : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' - 1))) < M.M i i' + 1

Tactic:
calc
      ℓ (π (alternatingWord i' i (M i i' - 1)))
      _ ≤ (alternatingWord i' i (M i i' - 1)).length := cs.length_wordProd_le _
      _ = M i i' - 1 := length_alternatingWord _ _ _
      _ ≤ M i i' := Nat.sub_le _ _
      _ < M i i' + 1 := Nat.lt_succ_self _

Premises used: CoxeterMatrix.M, HSub.hSub, Nat.lt_succ_self, Nat.sub_le, CoxeterSystem.alternatingWord, CoxeterSystem.length_wordProd_le, OfNat.ofNat, List.length, CoxeterSystem.length_alternatingWord
-- 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
m_1 : ℕ
hM : M.M i i' ≠ 0
m_2 : ℕ
m : (M.M i i').succ.le m_2
ih : ¬cs.IsReduced (alternatingWord i i' m_2)
step : ∀ (ih : cs.IsReduced (alternatingWord i i' m_2.succ)), cs.IsReduced (alternatingWord i i' m_2)
⊢ ¬cs.IsReduced (alternatingWord i i' m_2.succ)

Tactic:
contrapose ih