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
j : ℕ
⊢ (cs.rightInvSeq (take j ω.reverse.reverse).reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse
have rw : (cs.rightInvSeq (drop (ω.reverse.length - j) ω.reverse).reverse.reverse).reverse =
  (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse
Tactic: rw [List.take_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
t : W
i : B
ω : List B
ih : ∀ (ht : t ∈ cs.rightInvSeq ω), cs.IsReflection t
ht : t ∈ (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω
⊢ cs.IsReflection t
have cons : ∀
  (ih :
    ∀ (ht : (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω ∈ cs.rightInvSeq ω),
      cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)),
  cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)
Tactic: rcases ht with _ | ⟨_, mem⟩
Cleared hypotheses: t, ih, ht
-- 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
t : W
i : B
ω : List B
ih : ∀ (ht : t ∈ cs.rightInvSeq ω), cs.IsReflection t
ht : t ∈ (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω
cons :
  ∀
    (ih :
      ∀ (ht : (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω ∈ cs.rightInvSeq ω),
        cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)),
    cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)
⊢ cs.IsReflection t
have cons₁ : ∀ (mem : Mem t (cs.rightInvSeq ω)), cs.IsReflection t
Tactic: rcases ht with _ | ⟨_, mem⟩
Cleared hypotheses: ht
-- 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 : B
ω : List B
ih :
  ∀ (ht : (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω ∈ cs.rightInvSeq ω),
    cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)
⊢ cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)
have h : (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω = (cs.wordProd ω)⁻¹ * cs.simple i * (cs.wordProd ω)⁻¹⁻¹
Tactic: use (π ω)⁻¹, i
-- 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
t : W
ht : t ∈ cs.rightInvSeq ω
⊢ cs.IsReflection t
have nil : ∀ (ht : t ∈ cs.rightInvSeq []), cs.IsReflection t
Tactic: induction ω with
  | nil => simp at ht
  | cons i ω ih =>
    dsimp [rightInvSeq] at ht
    rcases ht with _ | ⟨_, mem⟩
    · use (π ω)⁻¹, i
      group
    · exact ih mem
Cleared hypotheses: ω, ht
-- 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
t : W
ht : t ∈ cs.rightInvSeq ω
nil : ∀ (ht : t ∈ cs.rightInvSeq []), cs.IsReflection t
⊢ cs.IsReflection t
have cons : ∀ (i : B) (ω : List B) (ih : ∀ (ht : t ∈ cs.rightInvSeq ω), cs.IsReflection t) (ht : t ∈ cs.rightInvSeq (i :: ω)),
  cs.IsReflection t
Tactic: induction ω with
  | nil => simp at ht
  | cons i ω ih =>
    dsimp [rightInvSeq] at ht
    rcases ht with _ | ⟨_, mem⟩
    · use (π ω)⁻¹, i
      group
    · exact ih mem
Cleared hypotheses: ω, ht
-- 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
t : W
ht : t ∈ cs.leftInvSeq ω
⊢ cs.IsReflection t
have ht₁ : t ∈ cs.rightInvSeq ω.reverse
Tactic: simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse, mem_reverse] at ht
Cleared hypotheses: ht
-- 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
j : ℕ
⊢ cs.wordProd ω * (cs.rightInvSeq ω).getD j 1 = cs.wordProd (ω.eraseIdx j)
have rw : cs.wordProd ω *
    ((cs.wordProd (drop (j + 1) ω))⁻¹ *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
      cs.wordProd (drop (j + 1) ω)) =
  cs.wordProd (take j ω ++ drop (j + 1) ω)
Tactic: rw [getD_rightInvSeq, eraseIdx_eq_take_drop_succ]
-- 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
j : ℕ
⊢ cs.wordProd ω *
      ((cs.wordProd (drop (j + 1) ω))⁻¹ *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        cs.wordProd (drop (j + 1) ω)) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
have nth_rw : cs.wordProd (take (j + 1) ω ++ drop (j + 1) ω) *
    ((cs.wordProd (drop (j + 1) ω))⁻¹ *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
      cs.wordProd (drop (j + 1) ω)) =
  cs.wordProd (take j ω ++ drop (j + 1) ω)
Tactic: nth_rw 1 [← take_append_drop (j + 1) ω]
-- 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
j : ℕ
⊢ cs.wordProd (take (j + 1) ω ++ drop (j + 1) ω) *
      ((cs.wordProd (drop (j + 1) ω))⁻¹ *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        cs.wordProd (drop (j + 1) ω)) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
have rw : cs.wordProd (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) *
    ((cs.wordProd (drop (j + 1) ω))⁻¹ *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
      cs.wordProd (drop (j + 1) ω)) =
  cs.wordProd (take j ω ++ drop (j + 1) ω)
Tactic: rw [take_add_one]
-- 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
j : ℕ
⊢ cs.wordProd
        (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) *
      ((cs.wordProd (drop (j + 1) ω))⁻¹ *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        cs.wordProd (drop (j + 1) ω)) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
have inl : ∀ (lt : j < ω.length),
  cs.wordProd
        (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) *
      ((cs.wordProd (drop (j + 1) ω))⁻¹ *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        cs.wordProd (drop (j + 1) ω)) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
Tactic: obtain lt | le := lt_or_ge j ω.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
j : ℕ
inl :
  ∀ (lt : j < ω.length),
    cs.wordProd
          (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) *
        ((cs.wordProd (drop (j + 1) ω))⁻¹ *
            (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
          cs.wordProd (drop (j + 1) ω)) =
      cs.wordProd (take j ω ++ drop (j + 1) ω)
⊢ cs.wordProd
        (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) *
      ((cs.wordProd (drop (j + 1) ω))⁻¹ *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        cs.wordProd (drop (j + 1) ω)) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
have inr : ∀ (le : ω.length ≤ j),
  cs.wordProd
        (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) *
      ((cs.wordProd (drop (j + 1) ω))⁻¹ *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        cs.wordProd (drop (j + 1) ω)) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
Tactic: obtain lt | le := lt_or_ge j ω.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
j : ℕ
lt : j < ω.length
⊢ cs.wordProd
        (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) *
      ((cs.wordProd (drop (j + 1) ω))⁻¹ *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        cs.wordProd (drop (j + 1) ω)) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
have inl : cs.wordProd (take j ω) *
    (cs.wordProd (some (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j lt)).toList *
      (cs.wordProd (drop (j + 1) ω) *
        ((cs.wordProd (drop (j + 1) ω))⁻¹ *
          ((Option.map cs.simple (some (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j lt))).getD 1 *
            cs.wordProd (drop (j + 1) ω))))) =
  cs.wordProd (take j ω) * cs.wordProd (drop (j + 1) ω)
Tactic: simp only [getElem?_eq_getElem lt, wordProd_append, mul_assoc]
-- 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
j : ℕ
le : ω.length ≤ j
⊢ cs.wordProd
        (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) *
      ((cs.wordProd (drop (j + 1) ω))⁻¹ *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        cs.wordProd (drop (j + 1) ω)) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
have inr : cs.wordProd (take j ω ++ Option.toList none ++ drop (j + 1) ω) *
    ((cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple none).getD 1 * cs.wordProd (drop (j + 1) ω)) =
  cs.wordProd (take j ω ++ drop (j + 1) ω)
Tactic: simp only [getElem?_eq_none 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
j : ℕ
⊢ (cs.leftInvSeq ω).getD j 1 * cs.wordProd ω = cs.wordProd (ω.eraseIdx j)
have rw : cs.wordProd (take j ω) *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
      (cs.wordProd (take j ω))⁻¹ *
    cs.wordProd ω =
  cs.wordProd (take j ω ++ drop (j + 1) ω)
Tactic: rw [getD_leftInvSeq, eraseIdx_eq_take_drop_succ]
-- 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
j : ℕ
⊢ cs.wordProd (take j ω) *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd ω =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
have nth_rw : cs.wordProd (take j ω) *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
      (cs.wordProd (take j ω))⁻¹ *
    cs.wordProd (take (j + 1) ω ++ drop (j + 1) ω) =
  cs.wordProd (take j ω ++ drop (j + 1) ω)
Tactic: nth_rw 4 [← take_append_drop (j + 1) ω]
-- 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
j : ℕ
⊢ cs.wordProd (take j ω) *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd (take (j + 1) ω ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
have rw : cs.wordProd (take j ω) *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
      (cs.wordProd (take j ω))⁻¹ *
    cs.wordProd
      (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) =
  cs.wordProd (take j ω ++ drop (j + 1) ω)
Tactic: rw [take_add_one]
-- 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
j : ℕ
⊢ cs.wordProd (take j ω) *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd
        (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
have inl : ∀ (lt : j < ω.length),
  cs.wordProd (take j ω) *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd
        (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
Tactic: obtain lt | le := lt_or_ge j ω.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
j : ℕ
inl :
  ∀ (lt : j < ω.length),
    cs.wordProd (take j ω) *
            (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
          (cs.wordProd (take j ω))⁻¹ *
        cs.wordProd
          (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) =
      cs.wordProd (take j ω ++ drop (j + 1) ω)
⊢ cs.wordProd (take j ω) *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd
        (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
have inr : ∀ (le : ω.length ≤ j),
  cs.wordProd (take j ω) *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd
        (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
Tactic: obtain lt | le := lt_or_ge j ω.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
j : ℕ
lt : j < ω.length
⊢ cs.wordProd (take j ω) *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd
        (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
have inl : cs.wordProd (take j ω) *
    ((Option.map cs.simple (some (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j lt))).getD 1 *
      ((cs.wordProd (take j ω))⁻¹ *
        (cs.wordProd (take j ω) *
          (cs.wordProd (some (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j lt)).toList *
            cs.wordProd (drop (j + 1) ω))))) =
  cs.wordProd (take j ω) * cs.wordProd (drop (j + 1) ω)
Tactic: simp only [getElem?_eq_getElem lt, wordProd_append, mul_assoc]
-- 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
j : ℕ
le : ω.length ≤ j
⊢ cs.wordProd (take j ω) *
          (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
        (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd
        (take j ω ++ (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j).toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
have inr : cs.wordProd (take j ω) * (Option.map cs.simple none).getD 1 * (cs.wordProd (take j ω))⁻¹ *
    cs.wordProd (take j ω ++ Option.toList none ++ drop (j + 1) ω) =
  cs.wordProd (take j ω ++ drop (j + 1) ω)
Tactic: simp only [getElem?_eq_none 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
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.rightInvSeq ω
⊢ cs.IsRightInversion (cs.wordProd ω) t
have left : cs.IsReflection t
Tactic: constructor
-- 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
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.rightInvSeq ω
left : cs.IsReflection t
⊢ cs.IsRightInversion (cs.wordProd ω) t
have right : cs.length (cs.wordProd ω * t) < cs.length (cs.wordProd ω)
Tactic: constructor
-- 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
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.rightInvSeq ω
⊢ cs.length (cs.wordProd ω * t) < cs.length (cs.wordProd ω)
have right : ∀ (j : ℕ) (hj : j < (cs.rightInvSeq ω).length)
  (ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj ∈ cs.rightInvSeq ω),
  cs.length (cs.wordProd ω * getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj) <
    cs.length (cs.wordProd ω)
Tactic: obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp ht
Cleared hypotheses: t, ht
-- 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
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.rightInvSeq ω).length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj ∈ cs.rightInvSeq ω
⊢ cs.length (cs.wordProd ω * getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj) <
    cs.length (cs.wordProd ω)
have right : cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)
Tactic: rw [← List.getD_eq_getElem _ 1 hj, 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
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.rightInvSeq ω).length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj ∈ cs.rightInvSeq ω
⊢ cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)
have hj₁ : j < ω.length
Tactic: rw [cs.length_rightInvSeq] at hj
Cleared hypotheses: ht
-- 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
hω : cs.IsReduced ω
j : ℕ
hj_1 : j < (cs.rightInvSeq ω).length
hj : j < ω.length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj_1 ∈ cs.rightInvSeq ω
⊢ (ω.eraseIdx j).length < ω.length
have rw : (ω.eraseIdx j).length < (ω.eraseIdx j).length + 1
Tactic: rw [← List.length_eraseIdx_add_one hj]
-- 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
hω : cs.IsReduced ω
j : ℕ
hj_1 : j < (cs.rightInvSeq ω).length
hj : j < ω.length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j hj_1 ∈ cs.rightInvSeq ω
⊢ cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)
have ℓ : (ω.eraseIdx j).length < ω.length
Tactic: calc
      ℓ (π (ω.eraseIdx j))
      _ ≤ (ω.eraseIdx j).length := cs.length_wordProd_le _
      _ < ω.length := by rw [← List.length_eraseIdx_add_one hj]; exact lt_add_one _
      _ = ℓ (π ω) := hω.symm
-- 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
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.leftInvSeq ω
⊢ cs.IsLeftInversion (cs.wordProd ω) t
have left : cs.IsReflection t
Tactic: constructor
-- 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
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.leftInvSeq ω
left : cs.IsReflection t
⊢ cs.IsLeftInversion (cs.wordProd ω) t
have right : cs.length (t * cs.wordProd ω) < cs.length (cs.wordProd ω)
Tactic: constructor
-- 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
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.leftInvSeq ω
⊢ cs.length (t * cs.wordProd ω) < cs.length (cs.wordProd ω)
have right : ∀ (j : ℕ) (hj : j < (cs.leftInvSeq ω).length)
  (ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj ∈ cs.leftInvSeq ω),
  cs.length (getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj * cs.wordProd ω) <
    cs.length (cs.wordProd ω)
Tactic: obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp ht
Cleared hypotheses: t, ht
-- 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
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.leftInvSeq ω).length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj ∈ cs.leftInvSeq ω
⊢ cs.length (getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj * cs.wordProd ω) <
    cs.length (cs.wordProd ω)
have right : cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)
Tactic: rw [← List.getD_eq_getElem _ 1 hj, getD_leftInvSeq_mul_wordProd]
-- 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
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.leftInvSeq ω).length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj ∈ cs.leftInvSeq ω
⊢ cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)
have hj₁ : j < ω.length
Tactic: rw [cs.length_leftInvSeq] at hj
Cleared hypotheses: ht
-- 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
hω : cs.IsReduced ω
j : ℕ
hj_1 : j < (cs.leftInvSeq ω).length
hj : j < ω.length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj_1 ∈ cs.leftInvSeq ω
⊢ (ω.eraseIdx j).length < ω.length
have rw : (ω.eraseIdx j).length < (ω.eraseIdx j).length + 1
Tactic: rw [← List.length_eraseIdx_add_one hj]
-- 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
hω : cs.IsReduced ω
j : ℕ
hj_1 : j < (cs.leftInvSeq ω).length
hj : j < ω.length
ht : getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j hj_1 ∈ cs.leftInvSeq ω
⊢ cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)
have ℓ : (ω.eraseIdx j).length < ω.length
Tactic: calc
      ℓ (π (ω.eraseIdx j))
      _ ≤ (ω.eraseIdx j).length := cs.length_wordProd_le _
      _ < ω.length := by rw [← List.length_eraseIdx_add_one hj]; exact lt_add_one _
      _ = ℓ (π ω) := hω.symm