apply Set.ext
case h'
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
⊢ {x | x ∈ s → x ∈ ∅} = sᶜ
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ᶜ