no goals
ι : Type ?u.473637
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s : List α
⊢ prod s = ∏ m in toFinset s, m ^ count m s
simpa using prod_list_map_count s id