no goals
α : Type u_1
β : Type ?u.355480
γ : Type ?u.355483
inst✝ : DecidableEq α
a : α
n : ℕ
s : Multiset α
⊢ count a (n • s) = n * count a s
induction n <;> simp [*, succ_nsmul', succ_mul, zero_nsmul]