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