no goals
ι : Type ?u.112709
α : Type ?u.112712
M : Type ?u.112715
N : Type ?u.112718
P : Type ?u.112721
M₀ : Type ?u.112724
G : Type u_1
R : Type ?u.112730
inst✝ : Group G
⊢ (prod [])⁻¹ = prod (reverse (map (fun x => x⁻¹) []))
simp
no goals
ι : Type ?u.112709
α : Type ?u.112712
M : Type ?u.112715
N : Type ?u.112718
P : Type ?u.112721
M₀ : Type ?u.112724
G : Type u_1
R : Type ?u.112730
inst✝ : Group G
x : G
xs : List G
⊢ (prod (x :: xs))⁻¹ = prod (reverse (map (fun x => x⁻¹) (x :: xs)))
simp [prod_inv_reverse xs]