apply Iff.intro
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ ¬sᶜ ∈ f ↔ s ∈ f
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