apply le_of_inf_eq
α : Type u_1
f : Ultrafilter α
g : Filter α
hg : f.as_filter ⊓ g ≠ ⊥
⊢ f.as_filter ≤ g
case a
α : Type u_1
f : Ultrafilter α
g : Filter α
hg : f.as_filter ⊓ g ≠ ⊥
⊢ f.as_filter ⊓ g = f.as_filter