no goals
ι : Type ?u.39786
α : Type u_2
β : Type u_1
γ : Type ?u.39795
inst✝² : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f✝ g : ι → α
inst✝¹ : CommMonoid β
s : Multiset α
F : Type u_3
inst✝ : MonoidHomClass F α β
f : F
l : List α
⊢ prod (map (↑f) (Quotient.mk (List.isSetoid α) l)) = ↑f (prod (Quotient.mk (List.isSetoid α) l))
simp only [l.prod_hom f, quot_mk_to_coe, coe_map, coe_prod]