English
Symmetric statements: the products of lis ω and ris ω both yield the inverse of π ω.
Русский
Симметричные утверждения: произведения lis ω и ris ω дают обратное от π ω.
LaTeX
$$$\mathrm{prod}(\mathrm{lis}(\omega)) = (\pi(\omega))^{-1}$$$
Lean4
theorem prod_leftInvSeq (ω : List B) : prod (lis ω) = (π ω)⁻¹ :=
by
simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse, prod_reverse_noncomm, inv_inj]
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 _
rw [this]
nth_rw 2 [← reverse_reverse ω]
rw [wordProd_reverse]
exact cs.prod_rightInvSeq _
