no goals
ι : Type ?u.39549
α✝ : Type ?u.39552
M : Type ?u.39555
N : Type ?u.39558
P : Type ?u.39561
M₀ : Type ?u.39564
G : Type ?u.39567
R : Type ?u.39570
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : Monoid P
l✝ l₁ l₂ : List M
a : M
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : HasDistribNeg α
l : List α
⊢ prod (map Neg.neg l) = (-1) ^ length l * prod l
simpa only [id_eq, neg_mul, one_mul, map_const', prod_replicate, map_id]
  using @prod_map_mul α α _ l (fun _ => -1) id