rw [Basis.le_def]
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
⊢ as_basis f ≤' b
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
⊢ ∀ (s : Set α), s ∈ b → ∃ t, t ∈ as_basis f ∧ t ⊆ s