-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem getD_rightInvSeq (ω : List B) (j : ℕ) :
    (ris ω).getD j 1 =
      (π (ω.drop (j + 1)))⁻¹
        * (Option.map (cs.simple) ω[j]?).getD 1
        * π (ω.drop (j + 1))

Proof state:
case cons.zero
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 ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)
⊢ ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω).getD 0 1 =
    (cs.wordProd (drop (0 + 1) (i :: ω)))⁻¹ * (Option.map cs.simple (i :: ω)[0]?).getD 1 *
      cs.wordProd (drop (0 + 1) (i :: ω))

Tactic:
simp [getD_cons_zero]

Result:
no goals

Proof state:
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 ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)

Tactic:
induction' ω with i ω ih generalizing j

Result:
case nil
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 [][j]?).getD 1 * cs.wordProd (drop (j + 1) [])

case cons
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 ω[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 (i :: ω)[j]?).getD 1 *
      cs.wordProd (drop (j + 1) (i :: ω))

Proof state:
case cons.succ
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 ω[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 (i :: ω)[j' + 1]?).getD 1 *
      cs.wordProd (drop (j' + 1 + 1) (i :: ω))

Tactic:
simp only [getD_eq_getElem?_getD, get?_eq_getElem?] at ih

Result:
case cons.succ
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 : ℕ),
    (cs.rightInvSeq ω)[j]?.getD 1 =
      (cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[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 (i :: ω)[j' + 1]?).getD 1 *
      cs.wordProd (drop (j' + 1 + 1) (i :: ω))

Proof state:
case cons.succ
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 : ℕ),
    (cs.rightInvSeq ω)[j]?.getD 1 =
      (cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[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 (i :: ω)[j' + 1]?).getD 1 *
      cs.wordProd (drop (j' + 1 + 1) (i :: ω))

Tactic:
simp [getD_cons_succ, ih j']

Result:
no goals

Proof state:
case nil
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 [][j]?).getD 1 * cs.wordProd (drop (j + 1) [])

Tactic:
simp

Result:
no goals

Proof state:
case cons
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 ω[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 (i :: ω)[j]?).getD 1 *
      cs.wordProd (drop (j + 1) (i :: ω))

Tactic:
rcases j with _ | j'

Result:
case cons.zero
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 ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)
⊢ ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω).getD 0 1 =
    (cs.wordProd (drop (0 + 1) (i :: ω)))⁻¹ * (Option.map cs.simple (i :: ω)[0]?).getD 1 *
      cs.wordProd (drop (0 + 1) (i :: ω))

case cons.succ
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 ω[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 (i :: ω)[j' + 1]?).getD 1 *
      cs.wordProd (drop (j' + 1 + 1) (i :: ω))

Proof state:
case cons
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 ω[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 (i :: ω)[j]?).getD 1 *
      cs.wordProd (drop (j + 1) (i :: ω))

Tactic:
dsimp only [rightInvSeq]

Result:
case cons
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 ω[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 (i :: ω)[j]?).getD 1 *
      cs.wordProd (drop (j + 1) (i :: ω))