no goals
ι : Type ?u.19659
α : Type u_1
β : Type u_2
F : Type u_3
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : F
⊢ ∀ (a : List (Set α)),
    ↑f '' Multiset.prod (Quotient.mk (List.isSetoid (Set α)) a) =
      Multiset.prod (Multiset.map (fun s => ↑f '' s) (Quotient.mk (List.isSetoid (Set α)) a))
simpa only [Multiset.quot_mk_to_coe, Multiset.coe_prod, Multiset.coe_map] using
  image_list_prod f