-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem rightInvSeq_concat (ω : List B) (i : B) :
    ris (ω.concat i) = (List.map (MulAut.conj (s i)) (ris ω)).concat (s i)

Proof state:
case cons
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) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)
⊢ (cs.wordProd (ω.concat i))⁻¹ * cs.simple j * cs.wordProd (ω.concat i) ::
      (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i) =
    cs.simple i * ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω) * (cs.simple i)⁻¹ ::
      (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)

Tactic:
simp only [concat_eq_append, wordProd_append, wordProd_cons, wordProd_nil, mul_one, mul_inv_rev,
  inv_simple, cons_append, cons.injEq, and_true]

Result:
case cons
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) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)
⊢ 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

Proof state:
case cons
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) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (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)⁻¹ ::
      (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)

Tactic:
rw [ih]

Result:
case cons
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) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)
⊢ (cs.wordProd (ω.concat i))⁻¹ * cs.simple j * cs.wordProd (ω.concat i) ::
      (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i) =
    cs.simple i * ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω) * (cs.simple i)⁻¹ ::
      (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)

Proof state:
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) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)

Tactic:
induction' ω with j ω ih

Result:
case nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.rightInvSeq ([].concat i) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq [])).concat (cs.simple i)

case cons
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) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)
⊢ cs.rightInvSeq ((j :: ω).concat i) =
    (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq (j :: ω))).concat (cs.simple i)

Proof state:
case cons
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) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)
⊢ cs.rightInvSeq ((j :: ω).concat i) =
    (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq (j :: ω))).concat (cs.simple i)

Tactic:
dsimp [rightInvSeq, concat]

Result:
case cons
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) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (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)⁻¹ ::
      (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)

Proof state:
case cons
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) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)
⊢ 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:
group

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
i : B
⊢ cs.rightInvSeq ([].concat i) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq [])).concat (cs.simple i)

Tactic:
simp

Result:
no goals