no goals
ι : Type ?u.290155
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
⊢ List.prod (List.map f (toList s)) = Finset.prod s f
rw [Finset.prod, ← Multiset.coe_prod, ← Multiset.coe_map, Finset.coe_toList]