awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ (cs.rightInvSeq ω).prod = (cs.wordProd ω)⁻¹
have nil : (cs.rightInvSeq []).prod = (cs.wordProd [])⁻¹
Tactic: induction ω with
  | nil => simp
  | cons i ω ih => simp [rightInvSeq, ih, wordProd_cons]
Cleared hypotheses: ω
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
nil : (cs.rightInvSeq []).prod = (cs.wordProd [])⁻¹
⊢ (cs.rightInvSeq ω).prod = (cs.wordProd ω)⁻¹
have cons : ∀ (i : B) (ω : List B) (ih : (cs.rightInvSeq ω).prod = (cs.wordProd ω)⁻¹),
  (cs.rightInvSeq (i :: ω)).prod = (cs.wordProd (i :: ω))⁻¹
Tactic: induction ω with
  | nil => simp
  | cons i ω ih => simp [rightInvSeq, ih, wordProd_cons]
Cleared hypotheses: ω
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ (cs.leftInvSeq ω).prod = (cs.wordProd ω)⁻¹
have simp : prod (List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse)) = cs.wordProd ω
Tactic: simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse, prod_reverse_noncomm, inv_inj]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = List.map id (cs.rightInvSeq ω.reverse)
have h : ∀ a ∈ cs.rightInvSeq ω.reverse, a⁻¹ = id a
Tactic: apply List.map_congr_left
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ prod (List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse)) = cs.wordProd ω
have this : List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
Tactic: have : List.map (fun x ↦ x⁻¹) (ris ω.reverse) = ris ω.reverse := calc
    List.map (fun x ↦ x⁻¹) (ris ω.reverse)
    _ = List.map id (ris ω.reverse) := by
        apply List.map_congr_left
        intro t ht
        exact (cs.isReflection_of_mem_rightInvSeq _ ht).inv
    _ = ris ω.reverse := map_id _
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
this : List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ prod (List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse)) = cs.wordProd ω
have rw : (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
this : List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω
have nth_rw : (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω.reverse.reverse
Tactic: nth_rw 2 [← reverse_reverse ω]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
this : List.map (fun (x : W) ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω.reverse.reverse
have rw : (cs.rightInvSeq ω.reverse).prod = (cs.wordProd ω.reverse)⁻¹
Tactic: rw [wordProd_reverse]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
⊢ (cs.rightInvSeq ω).Nodup
have apply : ∀ (i j : ℕ),
  i < j →
    j < (cs.rightInvSeq ω).length →
      getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) i ≠
        getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j
Tactic: apply List.nodup_iff_getElem?_ne_getElem?.mpr
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < (cs.rightInvSeq ω).length
dup :
  getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j =
    getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j'
⊢ False
have j'_lt_length₁ : j' < ω.length
Tactic: replace j'_lt_length : j' < List.length ω := by simpa using j'_lt_length
Cleared hypotheses: j'_lt_length
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
dup :
  getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j =
    getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j'
j'_lt_length : j' < ω.length
⊢ j < (cs.rightInvSeq ω).length
have simp : j < ω.length
Tactic: simp
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
dup :
  getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j =
    getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j'
j'_lt_length : j' < ω.length
⊢ False
have dup₁ : some (getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j sorry) =
  some (getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j' sorry)
Tactic: rw [getElem?_eq_getElem (by simp; lia), getElem?_eq_getElem (by simp; lia)] at dup
Cleared hypotheses: dup
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup :
  some (getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j ⋯) =
    some (getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j' ⋯)
⊢ False
have dup₁ : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j sorry =
  getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j' sorry
Tactic: apply Option.some_injective at dup
Cleared hypotheses: dup
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup :
  getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j ⋯ =
    getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j' ⋯
⊢ False
have dup₁ : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
Tactic: rw [← getD_eq_getElem _ 1, ← getD_eq_getElem _ 1] at dup
Cleared hypotheses: dup
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
⊢ False
have h₁ : let t := (cs.rightInvSeq ω).getD j 1;
t = (cs.rightInvSeq ω).getD j 1
Tactic: set! t := (ris ω).getD j 1 with h₁
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
⊢ False
have h₂ : let t' := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1;
t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
Tactic: set! t' := (ris (ω.eraseIdx j)).getD (j' - 1) 1 with h₂
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
⊢ False
have h₃ : t' = (cs.rightInvSeq ω).getD j' 1
Tactic: have h₃ : t' = (ris ω).getD j' 1 := by
    grind only [cs.getD_rightInvSeq, = eraseIdx_eq_take_drop_succ, = getElem?_eraseIdx,
      = drop_append, drop_of_length_le, drop_drop, = length_append, = length_take, = length_drop,
      = min_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
⊢ t * t' = 1
have rw : (cs.rightInvSeq ω).getD j' 1 * (cs.rightInvSeq ω).getD j' 1 = 1
Tactic: rw [h₁, h₃, dup]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
⊢ False
have h₄ : t * t' = 1
Tactic: have h₄ : t * t' = 1 := by
    rw [h₁, h₃, dup]
    exact cs.getD_rightInvSeq_mul_self _ _
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
⊢ cs.wordProd ω = cs.wordProd ω * t * t'
have rw : cs.wordProd ω = cs.wordProd ω * 1
Tactic: rw [mul_assoc, h₄]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
⊢ False
have h₅ : cs.wordProd ω = cs.wordProd ((ω.eraseIdx j).eraseIdx (j' - 1))
Tactic: have h₅ := calc
    π ω = π ω * t * t' := by rw [mul_assoc, h₄]; group
    _ = (π (ω.eraseIdx j)) * t' :=
        congrArg (· * t') (cs.wordProd_mul_getD_rightInvSeq _ _)
    _ = π ((ω.eraseIdx j).eraseIdx (j' - 1)) :=
        cs.wordProd_mul_getD_rightInvSeq _ _
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
h₅ : cs.wordProd ω = cs.wordProd ((ω.eraseIdx j).eraseIdx (j' - 1))
⊢ False
have h₆ : ω.length ≤ ((ω.eraseIdx j).eraseIdx (j' - 1)).length
Tactic: have h₆ := calc
    ω.length = ℓ (π ω) := rω.symm
    _ = ℓ (π ((ω.eraseIdx j).eraseIdx (j' - 1))) := congrArg cs.length h₅
    _ ≤ ((ω.eraseIdx j).eraseIdx (j' - 1)).length := cs.length_wordProd_le _
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
⊢ (cs.leftInvSeq ω).Nodup
have simp : (cs.rightInvSeq ω.reverse).Nodup
Tactic: simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse, nodup_reverse]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
⊢ (cs.rightInvSeq ω.reverse).Nodup
have rω₁ : cs.IsReduced ω.reverse
Tactic: apply nodup_rightInvSeq
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k < (cs.leftInvSeq (alternatingWord j i (2 * p))).length
have simp : k < 2 * p
Tactic: simp
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k < (alternatingWord j i (2 * p)).length
have simp : k < 2 * p
Tactic: simp
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq (alternatingWord i j (2 * p))) (k + 1) ⋯ =
    (((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
      (getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq (alternatingWord j i (2 * p))) k ⋯)
have rw : cs.wordProd (take (k + 1) (alternatingWord i j (2 * p))) *
      cs.simple (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) (k + 1) sorry) *
    (cs.wordProd (take (k + 1) (alternatingWord i j (2 * p))))⁻¹ =
  (((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
    (cs.wordProd (take k (alternatingWord j i (2 * p))) *
        cs.simple (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord j i (2 * p)) k sorry) *
      (cs.wordProd (take k (alternatingWord j i (2 * p))))⁻¹)
Tactic: rw [cs.getElem_leftInvSeq (alternatingWord i j (2 * p)) (k + 1) (by simp [h]),
    cs.getElem_leftInvSeq (alternatingWord j i (2 * p)) k (by simp; lia)]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ cs.wordProd (take (k + 1) (alternatingWord i j (2 * p))) *
        cs.simple
          (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) (k + 1) ⋯) *
      (cs.wordProd (take (k + 1) (alternatingWord i j (2 * p))))⁻¹ =
    (((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
      (cs.wordProd (take k (alternatingWord j i (2 * p))) *
          cs.simple (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord j i (2 * p)) k ⋯) *
        (cs.wordProd (take k (alternatingWord j i (2 * p))))⁻¹)
have simp : cs.simple (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) (k + 1) sorry) =
  cs.simple (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord j i (2 * p)) k sorry)
Tactic: simp only [MulAut.conj, listTake_succ_alternatingWord i j p k h, cs.wordProd_cons, mul_assoc,
    mul_inv_rev, inv_simple, MonoidHom.coe_mk, OneHom.coe_mk, MulEquiv.coe_mk, Equiv.coe_fn_mk,
    mul_right_inj, mul_left_inj]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : ℕ
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))
have zero : cs.simple (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (alternatingWord i j (2 * p)) 0 sorry) = cs.simple i
Tactic: 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
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
⊢ 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))
have succ : 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: 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
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 j i (2 * (k + 1)))
have 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)
Tactic: rw [(by ring : 2 * (k + 1) = 2 * k + 1 + 1), alternatingWord_succ j i, wordProd_concat]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
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))
have 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 sorry =
    cs.wordProd (alternatingWord j i (HMul.hMul (α := ℕ) 2 0 + 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]
Cleared hypotheses: i, j, k, h
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Inversion (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i 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))
⊢ 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))
have 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 sorry =
        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) sorry =
    cs.wordProd (alternatingWord j i (2 * (k + 1) + 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]
Cleared hypotheses: i, j, k, 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
⊢ ∃ (n : ℕ) (ω : List B), n = ω.length ∧ cs.wordProd ω = w
have rcases : ∀ (ω : List B), ∃ (n : ℕ) (ω_1 : List B), n = ω_1.length ∧ cs.wordProd ω_1 = cs.wordProd ω
Tactic: rcases cs.wordProd_surjective w with ⟨ω, 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
⊢ ∃ (n : ℕ) (ω_1 : List B), n = ω_1.length ∧ cs.wordProd ω_1 = cs.wordProd ω
have w : ℕ
Tactic: use ω.length, ω
-- 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
w : ℕ
w₁ : List B
⊢ ∃ (n : ℕ) (ω_1 : List B), n = ω_1.length ∧ cs.wordProd ω_1 = cs.wordProd ω
have h : ω.length = ω.length ∧ cs.wordProd ω = cs.wordProd ω
Tactic: use ω.length, ω
-- 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: obtain ⟨ω, hω, rfl⟩ := Nat.find_spec (cs.exists_word_with_prod w)
Cleared hypotheses: w