no goals
α : Type u_1
β : Type ?u.324507
γ : Type ?u.324510
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ Finset.Nonempty (filter p s) ↔ ∃ a, a ∈ s ∧ p a
simp [nonempty_iff_ne_empty, Ne.def, filter_eq_empty_iff, not_not, not_forall]