apply Iff.intro
α : Type u_1
f : Filter α
b : Basis α
⊢ as_basis f ≤' b ↔ f ≤ Basis.as_filter b
case mp
α : Type u_1
f : Filter α
b : Basis α
⊢ as_basis f ≤' b → f ≤ Basis.as_filter b

case mpr
α : Type u_1
f : Filter α
b : Basis α
⊢ f ≤ Basis.as_filter b → as_basis f ≤' b