rw [← Filter.empty_mem_iff_eq_bot, Filter.mem_inf_principal_iff] at h
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : f.as_filter ⊓ 𝓟 s = ⊥
⊢ False
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
⊢ False