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

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.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD j' ((MulAut.conj (cs.simple i)) 1) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (i :: ω)[j' + 1]?).getD ((MulAut.conj (cs.simple i)) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹

Tactic:
rw [getD_map]

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
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (MulAut.conj (cs.simple i)) ((cs.leftInvSeq ω).getD j' 1) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (i :: ω)[j' + 1]?).getD ((MulAut.conj (cs.simple i)) 1) *
      (cs.wordProd (take (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.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD j' 1 =
    cs.wordProd (take (j' + 1) (i :: ω)) * (Option.map cs.simple (i :: ω)[j' + 1]?).getD 1 *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹

Tactic:
rw [(by simp : 1 = ⇑(MulAut.conj (s i)) 1)]

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
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD j' ((MulAut.conj (cs.simple i)) 1) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (i :: ω)[j' + 1]?).getD ((MulAut.conj (cs.simple i)) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹

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

Tactic:
simp

Result:
no goals

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.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD (j' + 1) 1 =
    cs.wordProd (take (j' + 1) (i :: ω)) * (Option.map cs.simple (i :: ω)[j' + 1]?).getD 1 *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹

Tactic:
rw [getD_cons_succ]

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
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD j' 1 =
    cs.wordProd (take (j' + 1) (i :: ω)) * (Option.map cs.simple (i :: ω)[j' + 1]?).getD 1 *
      (cs.wordProd (take (j' + 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.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j : ℕ
⊢ (cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD j 1 =
    cs.wordProd (take j (i :: ω)) * (Option.map cs.simple (i :: ω)[j]?).getD 1 * (cs.wordProd (take j (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.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
⊢ (cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD 0 1 =
    cs.wordProd (take 0 (i :: ω)) * (Option.map cs.simple (i :: ω)[0]?).getD 1 * (cs.wordProd (take 0 (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.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD (j' + 1) 1 =
    cs.wordProd (take (j' + 1) (i :: ω)) * (Option.map cs.simple (i :: ω)[j' + 1]?).getD 1 *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹

Proof state:
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 ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ 1 = (MulAut.conj (cs.simple i)) 1

Tactic:
simp

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.leftInvSeq ω).getD j 1 = cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹

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.leftInvSeq []).getD j 1 =
    cs.wordProd (take j []) * (Option.map cs.simple [][j]?).getD 1 * (cs.wordProd (take j []))⁻¹

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.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j : ℕ
⊢ (cs.leftInvSeq (i :: ω)).getD j 1 =
    cs.wordProd (take j (i :: ω)) * (Option.map cs.simple (i :: ω)[j]?).getD 1 * (cs.wordProd (take j (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.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (MulAut.conj (cs.simple i))
      (cs.wordProd (take j' ω) * (Option.map cs.simple ω[j']?).getD 1 * (cs.wordProd (take j' ω))⁻¹) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (i :: ω)[j' + 1]?).getD ((MulAut.conj (cs.simple i)) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹

Tactic:
simp [← mul_assoc, wordProd_cons]

Result:
no goals