no goals
ι : Type ?u.114628
α : Type ?u.114631
M : Type ?u.114634
N : Type ?u.114637
P : Type ?u.114640
M₀ : Type ?u.114643
G : Type u_1
R : Type ?u.114649
inst✝ : Group G
⊢ ∀ (L : List G), prod (reverse L) = (prod (map (fun x => x⁻¹) L))⁻¹
simp [prod_inv_reverse]