apply Iff.intro
α : Type u_1
f g : Ultrafilter α
⊢ f.as_filter ≤ g.as_filter ↔ f = g
case mp
α : Type u_1
f g : Ultrafilter α
⊢ f.as_filter ≤ g.as_filter → f = g

case mpr
α : Type u_1
f g : Ultrafilter α
⊢ f = g → f.as_filter ≤ g.as_filter