rw [Set.mem_iff, Set.mem_compl_iff, Set.mem_empty_iff_false]
case h'.h
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
x : α
⊢ x ∈ {x | x ∈ s → x ∈ ∅} ↔ x ∈ sᶜ
no goals