rw [← as_basis_as_filter_eq_self f]
case mp
α : Type u_1
f : Filter α
b : Basis α
h : as_basis f ≤' b
⊢ f ≤ Basis.as_filter b
case mp
α : Type u_1
f : Filter α
b : Basis α
h : as_basis f ≤' b
⊢ Basis.as_filter (as_basis f) ≤ Basis.as_filter b