no goals
α : Type u_1
β : Type ?u.312315
γ : Type ?u.312318
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s : Multiset α
⊢ countp p (filter q s) = countp (fun a => p a ∧ q a) s
simp [countp_eq_card_filter]