no goals
ι : Type ?u.63333
α : Type u_1
β : Type ?u.63339
γ : Type ?u.63342
inst✝¹ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f g : ι → α
inst✝ : HasDistribNeg α
s : Multiset α
⊢ ∀ (a : List α),
    prod (map Neg.neg (Quotient.mk (List.isSetoid α) a)) =
      (-1) ^ ↑card (Quotient.mk (List.isSetoid α) a) * prod (Quotient.mk (List.isSetoid α) a)
simp