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
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD 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 ω))⁻¹
j' : ℕ
⊢ getD (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.leftInvSeq ω)) j'
      1 =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (i :: ω) (j' + 1))).getD
          1 *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹
have cons : getD (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.leftInvSeq ω)) j'
    ((((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) 1) =
  cs.wordProd (take (j' + 1) (i :: ω)) *
      (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (i :: ω) (j' + 1))).getD
        ((((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) 1) *
    (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹
Tactic: rw [(by simp : 1 = ⇑(MulAut.conj (s i)) 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
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD 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 ω))⁻¹
j' : ℕ
⊢ getD (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.leftInvSeq ω)) j'
      ((((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) 1) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (i :: ω) (j' + 1))).getD
          ((((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹
have cons : (((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) ((cs.leftInvSeq ω).getD j' 1) =
  cs.wordProd (take (j' + 1) (i :: ω)) *
      (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (i :: ω) (j' + 1))).getD
        ((((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) 1) *
    (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹
Tactic: rw [getD_map]
-- 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 :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD 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 ω))⁻¹
j' : ℕ
⊢ (((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) ((cs.leftInvSeq ω).getD j' 1) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (i :: ω) (j' + 1))).getD
          ((((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹
have cons : (((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
    (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) (i :: ω)) *
      (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (i :: ω) (j' + 1))).getD
        ((((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) 1) *
    (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹
Tactic: rw [ih j']
-- 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 (take j ω) *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
      (cs.wordProd (take j ω))⁻¹
have nil : ∀ (j : ℕ),
  (cs.leftInvSeq []).getD 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 []))⁻¹
Tactic: induction ω generalizing j with
  | nil => simp
  | cons i ω ih =>
    dsimp [leftInvSeq]
    rcases j with _ | j'
    · simp
    · rw [getD_cons_succ]
      rw [(by simp : 1 = ⇑(MulAut.conj (s i)) 1)]
      rw [getD_map]
      rw [ih j']
      simp [← mul_assoc, wordProd_cons]
Cleared hypotheses: ω, j
-- 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 : ℕ
nil :
  ∀ (j : ℕ),
    (cs.leftInvSeq []).getD 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.leftInvSeq ω).getD 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 ω))⁻¹
have cons : ∀ (i : B) (ω : List B)
  (ih :
    ∀ (j : ℕ),
      (cs.leftInvSeq ω).getD 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 ω))⁻¹)
  (j : ℕ),
  (cs.leftInvSeq (i :: ω)).getD j 1 =
    cs.wordProd (take j (i :: ω)) *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (i :: ω) j)).getD 1 *
      (cs.wordProd (take j (i :: ω)))⁻¹
Tactic: induction ω generalizing j with
  | nil => simp
  | cons i ω ih =>
    dsimp [leftInvSeq]
    rcases j with _ | j'
    · simp
    · rw [getD_cons_succ]
      rw [(by simp : 1 = ⇑(MulAut.conj (s i)) 1)]
      rw [getD_map]
      rw [ih j']
      simp [← mul_assoc, wordProd_cons]
Cleared hypotheses: ω, j
-- 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 : ℕ
h : j < ω.length
⊢ getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.leftInvSeq ω) j ⋯ =
    cs.wordProd (take j ω) * cs.simple (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j h) *
      (cs.wordProd (take 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 (take j ω) * cs.simple (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j h) *
    (cs.wordProd (take j ω))⁻¹
Tactic: rw [← List.getD_eq_getElem (lis ω) 1, getD_leftInvSeq]
-- 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 ω).getD j 1 * (cs.rightInvSeq ω).getD j 1 = 1
have simp_rw : (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 (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) ω))))) =
  1
Tactic: simp_rw [getD_rightInvSeq, 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 : ℕ
⊢ (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 (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) ω))))) =
    1
have inl : ∀ (hj : j < ω.length),
  (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 (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) ω))))) =
    1
Tactic: rcases em (j < ω.length) with hj | nhj
-- 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 :
  ∀ (hj : j < ω.length),
    (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 (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) ω))))) =
      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 (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) ω))))) =
    1
have inr : ∀ (nhj : ¬j < ω.length),
  (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 (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) ω))))) =
    1
Tactic: rcases em (j < ω.length) with hj | nhj
-- 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 : ℕ
hj : j < ω.length
⊢ (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 (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) ω))))) =
    1
have inl : (cs.wordProd (drop (j + 1) ω))⁻¹ *
    ((Option.map cs.simple (some (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j hj))).getD 1 *
      (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 hj))).getD 1 *
            cs.wordProd (drop (j + 1) ω))))) =
  1
Tactic: rw [getElem?_eq_getElem 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
j : ℕ
nhj : ¬j < ω.length
⊢ (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 (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) ω))))) =
    1
have inr : (cs.wordProd (drop (j + 1) ω))⁻¹ *
    ((Option.map cs.simple none).getD 1 *
      (cs.wordProd (drop (j + 1) ω) *
        ((cs.wordProd (drop (j + 1) ω))⁻¹ * ((Option.map cs.simple none).getD 1 * cs.wordProd (drop (j + 1) ω))))) =
  1
Tactic: rw [getElem?_eq_none_iff.mpr (by 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
ω : List B
j : ℕ
⊢ (cs.leftInvSeq ω).getD j 1 * (cs.leftInvSeq ω).getD j 1 = 1
have simp_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 ω) *
          ((Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
            (cs.wordProd (take j ω))⁻¹)))) =
  1
Tactic: simp_rw [getD_leftInvSeq, 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 : ℕ
⊢ 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 ω) *
            ((Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
              (cs.wordProd (take j ω))⁻¹)))) =
    1
have inl : ∀ (hj : 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 ω) *
            ((Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
              (cs.wordProd (take j ω))⁻¹)))) =
    1
Tactic: rcases em (j < ω.length) with hj | nhj
-- 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 :
  ∀ (hj : 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 ω) *
              ((Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
                (cs.wordProd (take 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 ω) *
            ((Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
              (cs.wordProd (take j ω))⁻¹)))) =
    1
have inr : ∀ (nhj : ¬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 ω) *
            ((Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
              (cs.wordProd (take j ω))⁻¹)))) =
    1
Tactic: rcases em (j < ω.length) with hj | nhj
-- 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 : ℕ
hj : 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 ω) *
            ((Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
              (cs.wordProd (take j ω))⁻¹)))) =
    1
have inl : cs.wordProd (take j ω) *
    ((Option.map cs.simple (some (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j hj))).getD 1 *
      ((cs.wordProd (take j ω))⁻¹ *
        (cs.wordProd (take j ω) *
          ((Option.map cs.simple (some (getElem (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j hj))).getD 1 *
            (cs.wordProd (take j ω))⁻¹)))) =
  1
Tactic: rw [getElem?_eq_getElem 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
j : ℕ
nhj : ¬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 ω) *
            ((Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) ω j)).getD 1 *
              (cs.wordProd (take j ω))⁻¹)))) =
    1
have inr : cs.wordProd (take j ω) *
    ((Option.map cs.simple none).getD 1 *
      ((cs.wordProd (take j ω))⁻¹ *
        (cs.wordProd (take j ω) * ((Option.map cs.simple none).getD 1 * (cs.wordProd (take j ω))⁻¹)))) =
  1
Tactic: rw [getElem?_eq_none_iff.mpr (by 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
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
k : B
ω : List B
tail_ih : cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)
⊢ cs.rightInvSeq (drop (j + 1) (k :: ω)) = drop (j + 1) (cs.rightInvSeq (k :: ω))
have succ : cs.rightInvSeq (drop j ω) = drop (j + 1) (cs.rightInvSeq (k :: ω))
Tactic: rw [drop_succ_cons, ih₁ ω, rightInvSeq, drop_succ_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
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
k : B
ω : List B
tail_ih : cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)
succ : cs.rightInvSeq (drop j ω) = drop (j + 1) (cs.rightInvSeq (k :: ω))
⊢ cs.rightInvSeq (drop (j + 1) (k :: ω)) = drop (j + 1) (cs.rightInvSeq (k :: ω))
have succ₁ : drop j (cs.rightInvSeq ω) = drop (j + 1) (cs.rightInvSeq (k :: ω))
Tactic: rw [drop_succ_cons, ih₁ ω, rightInvSeq, drop_succ_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
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
k : B
ω : List B
tail_ih : cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)
succ : cs.rightInvSeq (drop j ω) = drop (j + 1) (cs.rightInvSeq (k :: ω))
succ₁ : drop j (cs.rightInvSeq ω) = drop (j + 1) (cs.rightInvSeq (k :: ω))
⊢ cs.rightInvSeq (drop (j + 1) (k :: ω)) = drop (j + 1) (cs.rightInvSeq (k :: ω))
have succ₂ : drop j (cs.rightInvSeq ω) = drop (j + 1) ((cs.wordProd ω)⁻¹ * cs.simple k * cs.wordProd ω :: cs.rightInvSeq ω)
Tactic: rw [drop_succ_cons, ih₁ ω, rightInvSeq, drop_succ_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
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
k : B
ω : List B
tail_ih : cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)
succ : cs.rightInvSeq (drop j ω) = drop (j + 1) (cs.rightInvSeq (k :: ω))
succ₁ : drop j (cs.rightInvSeq ω) = drop (j + 1) (cs.rightInvSeq (k :: ω))
succ₂ : drop j (cs.rightInvSeq ω) = drop (j + 1) ((cs.wordProd ω)⁻¹ * cs.simple k * cs.wordProd ω :: cs.rightInvSeq ω)
⊢ cs.rightInvSeq (drop (j + 1) (k :: ω)) = drop (j + 1) (cs.rightInvSeq (k :: ω))
have succ₃ : drop j (cs.rightInvSeq ω) = drop j (cs.rightInvSeq ω)
Tactic: rw [drop_succ_cons, ih₁ ω, rightInvSeq, drop_succ_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
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
ω : List B
⊢ cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)
have succ : cs.rightInvSeq (drop (j + 1) []) = drop (j + 1) (cs.rightInvSeq [])
Tactic: induction ω with
    | nil => simp
    | cons k ω _ => rw [drop_succ_cons, ih₁ ω, rightInvSeq, drop_succ_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
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
ω : List B
succ : cs.rightInvSeq (drop (j + 1) []) = drop (j + 1) (cs.rightInvSeq [])
⊢ cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)
have succ₁ : ∀ (k : B) (ω : List B),
  cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω) →
    cs.rightInvSeq (drop (j + 1) (k :: ω)) = drop (j + 1) (cs.rightInvSeq (k :: ω))
Tactic: induction ω with
    | nil => simp
    | cons k ω _ => rw [drop_succ_cons, ih₁ ω, rightInvSeq, drop_succ_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
j : ℕ
⊢ cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
have zero : ∀ (ω : List B), cs.rightInvSeq (drop 0 ω) = drop 0 (cs.rightInvSeq ω)
Tactic: induction j generalizing ω with
  | zero => simp
  | succ j ih₁ =>
    induction ω with
    | nil => simp
    | cons k ω _ => rw [drop_succ_cons, ih₁ ω, rightInvSeq, drop_succ_cons]
Cleared hypotheses: ω, j
-- 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 : ℕ
zero : ∀ (ω : List B), cs.rightInvSeq (drop 0 ω) = drop 0 (cs.rightInvSeq ω)
⊢ cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
have succ : ∀ (j : ℕ) (ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)) (ω : List B),
  cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)
Tactic: induction j generalizing ω with
  | zero => simp
  | succ j ih₁ =>
    induction ω with
    | nil => simp
    | cons k ω _ => rw [drop_succ_cons, ih₁ ω, rightInvSeq, drop_succ_cons]
Cleared hypotheses: ω, j
-- 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 (take j ω) = take j (cs.leftInvSeq ω)
have simp : (cs.rightInvSeq (take j ω).reverse).reverse = take j (cs.rightInvSeq ω.reverse).reverse
Tactic: simp only [leftInvSeq_eq_reverse_rightInvSeq_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
j : ℕ
⊢ (cs.rightInvSeq (take j ω).reverse).reverse = take j (cs.rightInvSeq ω.reverse).reverse
have rw : (cs.rightInvSeq (take j ω).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
ω : List B
j : ℕ
⊢ (cs.rightInvSeq (take j ω).reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse
have nth_rw : (cs.rightInvSeq (take j ω.reverse.reverse).reverse).reverse =
  (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse
Tactic: nth_rw 1 [← List.reverse_reverse ω]