awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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) []
cons :
  ∀ (i : B) (ω : List B) (ih : (cs.rightInvSeq ω).length = ω.length), (cs.rightInvSeq (i :: ω)).length = (i :: ω).length
⊢ (cs.rightInvSeq ω).length = ω.length

Tactic:
induction ω with
  | nil => simp
  | cons i ω ih => simpa [rightInvSeq]

Premises used: List.cons, CoxeterSystem.rightInvSeq, List.nil
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ (cs.leftInvSeq ω).length = ω.length

Tactic:
simp [leftInvSeq_eq_reverse_rightInvSeq_reverse]

Premises used: _private.0.CoxeterSystem.leftInvSeq_eq_reverse_rightInvSeq_reverse
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
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:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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 :: ω))
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 :: ω))
⊢ ((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 :: ω))

Tactic:
rcases j with _ | j'
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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) ω)
⊢ ((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:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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' : ℕ
⊢ ∀ (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

Premises used: List.getD_eq_getElem?_getD
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
j' : ℕ
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) ω)
⊢ ((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:
simp [ih j']
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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) [])
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 :: ω))
⊢ (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']

Premises used: List.cons, CoxeterSystem.rightInvSeq, List.getD_eq_getElem?_getD, List.nil
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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
⊢ j < (cs.rightInvSeq ω).length

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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) ω)
rw₁ 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) ω)
⊢ 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) ω)

Tactic:
rw [← List.getD_eq_getElem (ris ω) 1, getD_rightInvSeq]

Premises used: CoxeterSystem.getD_rightInvSeq
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
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:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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 :: ω)))⁻¹
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 :: ω)))⁻¹
⊢ (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 :: ω)))⁻¹

Tactic:
rcases j with _ | j'
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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 ω))⁻¹
⊢ (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:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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 :
  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 :: ω)))⁻¹
⊢ (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:
rw [getD_cons_succ]

Premises used: List.getD_cons_succ
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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' : ℕ
⊢ Eq (α := W) (1 : W) ((((MulAut.conj : (a : W) → MulAut W) (cs.simple i) : MulAut W) : (a : W) → W) 1 : W)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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 :
  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 :: ω)))⁻¹
⊢ 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 [(by simp : 1 = ⇑(MulAut.conj (s i)) 1)]
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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 :
  (((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 :: ω)))⁻¹
⊢ 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 [getD_map]

Premises used: List.getD_map
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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 :
  (((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 :: ω)))⁻¹
⊢ (((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 [ih j']
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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.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:
simp [← mul_assoc, wordProd_cons]

Premises used: mul_assoc, CoxeterSystem.wordProd_cons
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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 []))⁻¹
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 :: ω)))⁻¹
⊢ (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]

Premises used: List.getD_map, mul_assoc, CoxeterSystem.wordProd_cons, List.getD_cons_succ, List.cons, CoxeterSystem.leftInvSeq, List.nil
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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
⊢ j < (cs.leftInvSeq ω).length

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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.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 ω))⁻¹
⊢ 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 ω))⁻¹

Tactic:
rw [← List.getD_eq_getElem (lis ω) 1, getD_leftInvSeq]

Premises used: CoxeterSystem.getD_leftInvSeq
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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
⊢ 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:
simp [h]
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
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
⊢ (cs.rightInvSeq ω).getD j 1 * (cs.rightInvSeq ω).getD j 1 = 1

Tactic:
simp_rw [getD_rightInvSeq, mul_assoc]

Premises used: mul_assoc, CoxeterSystem.getD_rightInvSeq
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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
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
⊢ (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

Premises used: em, LT.lt, List.length
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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
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
⊢ (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:
rw [getElem?_eq_getElem hj]

Premises used: List.getElem?_eq_getElem
-- Module: Mathlib.GroupTheory.Coxeter.Inversion
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 (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:
simp [← mul_assoc]

Premises used: mul_assoc