. rw [h'] at h
  exact hne h
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
h' : {x | x ∈ s → x ∈ ∅} = sᶜ
⊢ False

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