. intros hne
  rw [← mem_coe, ← Filter.le_principal_iff]
  apply le_of_inf_ne_bot
  intros h
  rw [← Filter.empty_mem_iff_eq_bot, Filter.mem_inf_principal_iff] at h
  suffices h' : {x | x ∈ s → x ∈ (∅ : Set α)} = sᶜ
  . rw [h'] at h
    exact hne h
  apply Set.ext; intros x
  rw [Set.mem_iff, Set.mem_compl_iff, Set.mem_empty_iff_false]
case mp
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ ¬sᶜ ∈ f → s ∈ f

case mpr
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ s ∈ f → ¬sᶜ ∈ f
case mpr
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ s ∈ f → ¬sᶜ ∈ f