no goals
ι : Type ?u.118773
α : Type ?u.118776
M : Type ?u.118779
N : Type ?u.118782
P : Type ?u.118785
M₀ : Type ?u.118788
G : Type u_1
R : Type ?u.118794
inst✝ : CommGroup G
⊢ (prod [])⁻¹ = prod (map (fun x => x⁻¹) [])
simp
no goals
ι : Type ?u.118773
α : Type ?u.118776
M : Type ?u.118779
N : Type ?u.118782
P : Type ?u.118785
M₀ : Type ?u.118788
G : Type u_1
R : Type ?u.118794
inst✝ : CommGroup G
x : G
xs : List G
⊢ (prod (x :: xs))⁻¹ = prod (map (fun x => x⁻¹) (x :: xs))
simp [mul_comm, prod_inv xs]