no goals
ι : Type ?u.13316
α : Type u_1
β : Type ?u.13322
γ : Type ?u.13325
inst✝ : CommMonoid α
s✝ t✝ : Multiset α
a : α
m : Multiset ι
f g : ι → α
s t : Multiset α
l₁ l₂ : List α
⊢ prod (Quotient.mk (List.isSetoid α) l₁ + Quotient.mk (List.isSetoid α) l₂) =
    prod (Quotient.mk (List.isSetoid α) l₁) * prod (Quotient.mk (List.isSetoid α) l₂)
simp