no goals
ι : Type ?u.936659
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
s : Multiset α
⊢ ∑ a in toFinset s, count a s • {a} = s
rw [← Finset.sum_multiset_map_count, Multiset.sum_map_singleton]