no goals
ι : Type ?u.497
α : Type u_1
β : Type u_2
F : Type u_3
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
f : F
a : Set α
as : List (Set α)
⊢ ↑f '' List.prod (a :: as) = List.prod (List.map (fun s => ↑f '' s) (a :: as))
rw [List.map_cons, List.prod_cons, List.prod_cons, image_mul, image_list_prod _ _]