no goals
α : Type ?u.13830
β : Type ?u.13833
ι : Type u_1
s : Finset ι
n : ℕ
⊢ ↑toMultiset (∑ i in s, single i n) = n • s.val
simp_rw [toMultiset_sum, Finsupp.toMultiset_single, sum_nsmul, sum_multiset_singleton]