no goals
ι : Type u_1
α : Type u_2
β : Type ?u.90981
F : Type ?u.90984
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : MonoidHomClass F α β
inst✝ : Fintype ι
S : ι → Set α
⊢ (fun f => ∏ i : ι, f i) '' pi univ S = ∏ i : ι, S i
simpa only [Finset.coe_univ] using image_finset_prod_pi Finset.univ S