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
t : W
ht : cs.IsReflection t
w : W
⊢ cs.length w < cs.length (w * t) ↔ cs.length w ≤ cs.length (w * t)
have mp : cs.length w < cs.length (w * t) → cs.length w ≤ cs.length (w * 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
t : W
ht : cs.IsReflection t
w : W
mp : cs.length w < cs.length (w * t) → cs.length w ≤ cs.length (w * t)
⊢ cs.length w < cs.length (w * t) ↔ cs.length w ≤ cs.length (w * t)
have mpr : cs.length w ≤ cs.length (w * t) → cs.length w < cs.length (w * 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
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsLeftInversion (t * w) t ↔ ¬cs.IsLeftInversion w t
have rw : cs.IsRightInversion (t * w)⁻¹ t ↔ ¬cs.IsLeftInversion w t
Tactic: rw [← isRightInversion_inv_iff, ← isRightInversion_inv_iff, mul_inv_rev, ht.inv,
    ht.isRightInversion_mul_left_iff]
-- 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
ht : cs.IsReflection t
w : W
rw : cs.IsRightInversion (t * w)⁻¹ t ↔ ¬cs.IsLeftInversion w t
⊢ cs.IsLeftInversion (t * w) t ↔ ¬cs.IsLeftInversion w t
have rw₁ : cs.IsRightInversion (t * w)⁻¹ t ↔ ¬cs.IsRightInversion w⁻¹ t
Tactic: rw [← isRightInversion_inv_iff, ← isRightInversion_inv_iff, mul_inv_rev, ht.inv,
    ht.isRightInversion_mul_left_iff]
-- 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
ht : cs.IsReflection t
w : W
rw : cs.IsRightInversion (t * w)⁻¹ t ↔ ¬cs.IsLeftInversion w t
rw₁ : cs.IsRightInversion (t * w)⁻¹ t ↔ ¬cs.IsRightInversion w⁻¹ t
⊢ cs.IsLeftInversion (t * w) t ↔ ¬cs.IsLeftInversion w t
have rw₂ : cs.IsRightInversion (w⁻¹ * t⁻¹) t ↔ ¬cs.IsRightInversion w⁻¹ t
Tactic: rw [← isRightInversion_inv_iff, ← isRightInversion_inv_iff, mul_inv_rev, ht.inv,
    ht.isRightInversion_mul_left_iff]
-- 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
ht : cs.IsReflection t
w : W
rw : cs.IsRightInversion (t * w)⁻¹ t ↔ ¬cs.IsLeftInversion w t
rw₁ : cs.IsRightInversion (t * w)⁻¹ t ↔ ¬cs.IsRightInversion w⁻¹ t
rw₂ : cs.IsRightInversion (w⁻¹ * t⁻¹) t ↔ ¬cs.IsRightInversion w⁻¹ t
⊢ cs.IsLeftInversion (t * w) t ↔ ¬cs.IsLeftInversion w t
have rw₃ : cs.IsRightInversion (w⁻¹ * t) t ↔ ¬cs.IsRightInversion w⁻¹ t
Tactic: rw [← isRightInversion_inv_iff, ← isRightInversion_inv_iff, mul_inv_rev, ht.inv,
    ht.isRightInversion_mul_left_iff]
-- 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
ht : cs.IsReflection t
w : W
rw : cs.IsRightInversion (t * w)⁻¹ t ↔ ¬cs.IsLeftInversion w t
rw₁ : cs.IsRightInversion (t * w)⁻¹ t ↔ ¬cs.IsRightInversion w⁻¹ t
rw₂ : cs.IsRightInversion (w⁻¹ * t⁻¹) t ↔ ¬cs.IsRightInversion w⁻¹ t
rw₃ : cs.IsRightInversion (w⁻¹ * t) t ↔ ¬cs.IsRightInversion w⁻¹ t
⊢ cs.IsLeftInversion (t * w) t ↔ ¬cs.IsLeftInversion w t
have rw₄ : ¬cs.IsRightInversion w⁻¹ t ↔ ¬cs.IsRightInversion w⁻¹ t
Tactic: rw [← isRightInversion_inv_iff, ← isRightInversion_inv_iff, mul_inv_rev, ht.inv,
    ht.isRightInversion_mul_left_iff]
-- 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
ω : List B
ih :
  cs.rightInvSeq (ω.concat i) =
    concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
      (cs.simple i)
⊢ cs.rightInvSeq ((j :: ω).concat i) =
    concat
      (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
        (cs.rightInvSeq (j :: ω)))
      (cs.simple i)
have cons : (cs.wordProd (ω.concat i))⁻¹ * cs.simple j * cs.wordProd (ω.concat i) :: cs.rightInvSeq (ω.concat i) =
  cs.simple i * ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω) * (cs.simple i)⁻¹ ::
    concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
      (cs.simple i)
Tactic: dsimp [rightInvSeq, 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
ω : List B
ih :
  cs.rightInvSeq (ω.concat i) =
    concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
      (cs.simple i)
⊢ (cs.wordProd (ω.concat i))⁻¹ * cs.simple j * cs.wordProd (ω.concat i) :: cs.rightInvSeq (ω.concat i) =
    cs.simple i * ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω) * (cs.simple i)⁻¹ ::
      concat
        (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
        (cs.simple i)
have cons : (cs.wordProd (ω.concat i))⁻¹ * cs.simple j * cs.wordProd (ω.concat i) ::
    concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
      (cs.simple i) =
  cs.simple i * ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω) * (cs.simple i)⁻¹ ::
    concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
      (cs.simple i)
Tactic: rw [ih]
-- 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
ω : List B
ih :
  cs.rightInvSeq (ω.concat i) =
    concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
      (cs.simple i)
⊢ (cs.wordProd (ω.concat i))⁻¹ * cs.simple j * cs.wordProd (ω.concat i) ::
      concat
        (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
        (cs.simple i) =
    cs.simple i * ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω) * (cs.simple i)⁻¹ ::
      concat
        (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
        (cs.simple i)
have cons : cs.simple i * (cs.wordProd ω)⁻¹ * cs.simple j * (cs.wordProd ω * cs.simple i) =
  cs.simple i * ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω) * cs.simple i
Tactic: simp only [concat_eq_append, wordProd_append, wordProd_cons, wordProd_nil, mul_one, mul_inv_rev,
      inv_simple, cons.injEq, and_true]
-- 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
i : B
⊢ cs.rightInvSeq (ω.concat i) =
    concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
      (cs.simple i)
have nil : cs.rightInvSeq (concat [] i) =
  concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq []))
    (cs.simple i)
Tactic: induction ω with
  | nil => simp
  | cons j ω ih =>
    dsimp [rightInvSeq, concat]
    rw [ih]
    simp only [concat_eq_append, wordProd_append, wordProd_cons, wordProd_nil, mul_one, mul_inv_rev,
      inv_simple, cons.injEq, and_true]
    group
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
i : B
nil :
  cs.rightInvSeq (concat [] i) =
    concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq []))
      (cs.simple i)
⊢ cs.rightInvSeq (ω.concat i) =
    concat (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
      (cs.simple i)
have cons : ∀ (j : B) (ω : List B)
  (ih :
    cs.rightInvSeq (ω.concat i) =
      concat
        (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.rightInvSeq ω))
        (cs.simple i)),
  cs.rightInvSeq ((j :: ω).concat i) =
    concat
      (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
        (cs.rightInvSeq (j :: ω)))
      (cs.simple i)
Tactic: induction ω with
  | nil => simp
  | cons j ω ih =>
    dsimp [rightInvSeq, concat]
    rw [ih]
    simp only [concat_eq_append, wordProd_append, wordProd_cons, wordProd_nil, mul_one, mul_inv_rev,
      inv_simple, cons.injEq, and_true]
    group
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
i : B
ω : List B
ih : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
⊢ cs.leftInvSeq (i :: ω) = (cs.rightInvSeq (i :: ω).reverse).reverse
have cons : cs.simple i ::
    List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
      (cs.rightInvSeq ω.reverse).reverse =
  (concat
      (List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
        (cs.rightInvSeq ω.reverse))
      (cs.simple i)).reverse
Tactic: rw [leftInvSeq, reverse_cons, ← concat_eq_append, rightInvSeq_concat, ih]
-- 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 ω = (cs.rightInvSeq ω.reverse).reverse
have nil : cs.leftInvSeq [] = (cs.rightInvSeq (reverse [])).reverse
Tactic: induction ω with
  | nil => simp
  | cons i ω ih =>
    rw [leftInvSeq, reverse_cons, ← concat_eq_append, rightInvSeq_concat, ih]
    simp [map_reverse]
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.leftInvSeq [] = (cs.rightInvSeq (reverse [])).reverse
⊢ cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
have cons : ∀ (i : B) (ω : List B) (ih : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse),
  cs.leftInvSeq (i :: ω) = (cs.rightInvSeq (i :: ω).reverse).reverse
Tactic: induction ω with
  | nil => simp
  | cons i ω ih =>
    rw [leftInvSeq, reverse_cons, ← concat_eq_append, rightInvSeq_concat, ih]
    simp [map_reverse]
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.rightInvSeq ω).length = ω.length
have nil : (cs.rightInvSeq []).length = List.length.{u_1} (α := B) []
Tactic: induction ω with
  | nil => simp
  | cons i ω ih => simpa [rightInvSeq]
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 []).length = List.length.{u_1} (α := B) []
⊢ (cs.rightInvSeq ω).length = ω.length
have cons : ∀ (i : B) (ω : List B) (ih : (cs.rightInvSeq ω).length = ω.length), (cs.rightInvSeq (i :: ω)).length = (i :: ω).length
Tactic: induction ω with
  | nil => simp
  | cons i ω ih => simpa [rightInvSeq]
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
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.rightInvSeq ω).getD 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) ω)
j : ℕ
⊢ ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω).getD j 1 =
    (cs.wordProd (drop (j + 1) (i :: ω)))⁻¹ *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (i :: ω) j)).getD 1 *
      cs.wordProd (drop (j + 1) (i :: ω))
have cons : ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω).getD 0 1 =
  (cs.wordProd (drop (HAdd.hAdd (α := ℕ) 0 1) (i :: ω)))⁻¹ *
      (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (i :: ω) 0)).getD 1 *
    cs.wordProd (drop (HAdd.hAdd (α := ℕ) 0 1) (i :: ω))
Tactic: rcases j with _ | j'
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
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.rightInvSeq ω).getD 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) ω)
j : ℕ
cons :
  ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω).getD 0 1 =
    (cs.wordProd (drop (HAdd.hAdd (α := ℕ) 0 1) (i :: ω)))⁻¹ *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (i :: ω) 0)).getD 1 *
      cs.wordProd (drop (HAdd.hAdd (α := ℕ) 0 1) (i :: ω))
⊢ ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω).getD j 1 =
    (cs.wordProd (drop (j + 1) (i :: ω)))⁻¹ *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (i :: ω) j)).getD 1 *
      cs.wordProd (drop (j + 1) (i :: ω))
have cons₁ : ∀ (j' : ℕ),
  ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω).getD (j' + 1) 1 =
    (cs.wordProd (drop (j' + 1 + 1) (i :: ω)))⁻¹ *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (i :: ω) (j' + 1))).getD
          1 *
      cs.wordProd (drop (j' + 1 + 1) (i :: ω))
Tactic: rcases j with _ | j'
Cleared hypotheses: j
-- 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
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.rightInvSeq ω).getD 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) ω)
j' : ℕ
⊢ ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω).getD (j' + 1) 1 =
    (cs.wordProd (drop (j' + 1 + 1) (i :: ω)))⁻¹ *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (i :: ω) (j' + 1))).getD
          1 *
      cs.wordProd (drop (j' + 1 + 1) (i :: ω))
have ih₁ : ∀ (j : ℕ),
  (getElem? (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) j).getD 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) ω)
Tactic: simp only [getD_eq_getElem?_getD] at ih
Cleared hypotheses: ih
-- 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.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) ω)
have nil : ∀ (j : ℕ),
  (cs.rightInvSeq []).getD 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) [])
Tactic: induction ω generalizing j with
  | nil => simp
  | cons i ω ih =>
    dsimp only [rightInvSeq]
    rcases j with _ | j'
    · simp
    · simp only [getD_eq_getElem?_getD] at ih
      simp [ih j']
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.rightInvSeq []).getD 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.rightInvSeq ω).getD 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) ω)
have cons : ∀ (i : B) (ω : List B)
  (ih :
    ∀ (j : ℕ),
      (cs.rightInvSeq ω).getD 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) ω))
  (j : ℕ),
  (cs.rightInvSeq (i :: ω)).getD j 1 =
    (cs.wordProd (drop (j + 1) (i :: ω)))⁻¹ *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (i :: ω) j)).getD 1 *
      cs.wordProd (drop (j + 1) (i :: ω))
Tactic: induction ω generalizing j with
  | nil => simp
  | cons i ω ih =>
    dsimp only [rightInvSeq]
    rcases j with _ | j'
    · simp
    · simp only [getD_eq_getElem?_getD] at ih
      simp [ih j']
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.rightInvSeq ω) 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) ω)
have rw : (cs.rightInvSeq ω).getD 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) ω)
Tactic: rw [← List.getD_eq_getElem (ris ω) 1, getD_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
ω : List B
j : ℕ
h : j < ω.length
rw :
  (cs.rightInvSeq ω).getD 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) ω)
⊢ getElem (valid := fun (as : List W) (i : ℕ) ↦ i < as.length) (cs.rightInvSeq ω) 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) ω)
have 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) ω)
Tactic: rw [← List.getD_eq_getElem (ris ω) 1, getD_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 : 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.simple i ::
          List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
            (cs.leftInvSeq ω)).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 :: ω)))⁻¹
have cons : (cs.simple i ::
        List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) (cs.leftInvSeq ω)).getD
    0 1 =
  cs.wordProd (take 0 (i :: ω)) *
      (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (i :: ω) 0)).getD 1 *
    (cs.wordProd (take 0 (i :: ω)))⁻¹
Tactic: rcases j with _ | j'
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
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 : ℕ
cons :
  (cs.simple i ::
          List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
            (cs.leftInvSeq ω)).getD
      0 1 =
    cs.wordProd (take 0 (i :: ω)) *
        (Option.map cs.simple (getElem? (valid := fun (as : List B) (i : ℕ) ↦ i < as.length) (i :: ω) 0)).getD 1 *
      (cs.wordProd (take 0 (i :: ω)))⁻¹
⊢ (cs.simple i ::
          List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
            (cs.leftInvSeq ω)).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 :: ω)))⁻¹
have cons₁ : ∀ (j' : ℕ),
  (cs.simple i ::
          List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
            (cs.leftInvSeq ω)).getD
      (j' + 1) 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 :: ω)))⁻¹
Tactic: rcases j with _ | j'
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
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.simple i ::
          List.map (⇑((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W)
            (cs.leftInvSeq ω)).getD
      (j' + 1) 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' 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 :: ω)))⁻¹
Tactic: rw [getD_cons_succ]