-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem prod_leftInvSeq (ω : List B) : prod (lis ω) = (π ω)⁻¹

Proof state:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ ∀ a ∈ cs.rightInvSeq ω.reverse, a⁻¹ = id a

Tactic:
intro t ht

Result:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
t : W
ht : t ∈ cs.rightInvSeq ω.reverse
⊢ t⁻¹ = id t

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ (cs.leftInvSeq ω).prod = (cs.wordProd ω)⁻¹

Tactic:
simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse, prod_reverse_noncomm, inv_inj]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ (List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse)).prod = cs.wordProd ω

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
this : List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω.reverse.reverse

Tactic:
rw [wordProd_reverse]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
this : List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (cs.rightInvSeq ω.reverse).prod = (cs.wordProd ω.reverse)⁻¹

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
this : List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω

Tactic:
nth_rw 2 [← reverse_reverse ω]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
this : List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω.reverse.reverse

Proof state:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
t : W
ht : t ∈ cs.rightInvSeq ω.reverse
⊢ t⁻¹ = id t

Tactic:
exact (cs.isReflection_of_mem_rightInvSeq _ ht).inv

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
⊢ List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse) = List.map id (cs.rightInvSeq ω.reverse)

Tactic:
apply List.map_congr_left

Result:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ ∀ a ∈ cs.rightInvSeq ω.reverse, a⁻¹ = id a

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
this : List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse)).prod = cs.wordProd ω

Tactic:
rw [this]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
this : List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
this : List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (cs.rightInvSeq ω.reverse).prod = (cs.wordProd ω.reverse)⁻¹

Tactic:
exact cs.prod_rightInvSeq _

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
⊢ (List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse)).prod = cs.wordProd ω

Tactic:
have : List.map (fun x ↦ x⁻¹) (ris ω.reverse) = ris ω.reverse := calc
  List.map (fun x ↦ x⁻¹) (ris ω.reverse)
  _ = List.map id (ris ω.reverse)             := by
      apply List.map_congr_left
      intro t ht
      exact (cs.isReflection_of_mem_rightInvSeq _ ht).inv
  _ = ris ω.reverse                           := map_id _

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
this : List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse)).prod = cs.wordProd ω