no goals
α : Type u_1
β : Type ?u.323235
γ : Type ?u.323238
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
h : ∀ (x : α), x ∈ s → ¬p x
⊢ ∀ (x : α), ¬x ∈ filter p s
simpa only [eq_empty_iff_forall_not_mem, mem_filter, not_and] using h