. exact eq_of_le
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
case mpr
α : Type u_1
f g : Ultrafilter α
⊢ f = g → f.as_filter ≤ g.as_filter