no goals
α : Type u_1
β : Type ?u.417033
γ : Type ?u.417036
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s t : Finset α
⊢ filter p s ∩ filter (fun a => ¬p a) t = ∅
simpa using (disjoint_filter_filter_neg s t p).eq_bot