no goals
α : Type u_1
β : Type ?u.311172
γ : Type ?u.311175
p : α → Prop
inst✝ : DecidablePred p
s t : Multiset α
h : s ≤ t
⊢ countp p s ≤ countp p t
simpa [countp_eq_card_filter] using card_le_of_le (filter_le_filter p h)