rw [← empty_mem_iff_eq_bot, ← Set.compl_inter_self s]
α : Type u_1
f : Filter α
s : Set α
hf : f ≠ ⊥
h : s ∈ f
h' : sᶜ ∈ f
⊢ f = ⊥
α : Type u_1
f : Filter α
s : Set α
hf : f ≠ ⊥
h : s ∈ f
h' : sᶜ ∈ f
⊢ sᶜ ∩ s ∈ f