. intros h
  rw [← as_basis_as_filter_eq_self f]
  exact Basis.as_filter_le h
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
case mpr
α : Type u_1
f : Filter α
b : Basis α
⊢ f ≤ Basis.as_filter b → as_basis f ≤' b