no goals
α : Type u_1
β : Type ?u.300349
γ : Type ?u.300352
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ countp p (n • s) = n * countp p s
induction n <;> simp [*, succ_nsmul', succ_mul, zero_nsmul]