. intros h
  rw [Basis.le_def]
  intros s hs
  have hs' := h s (Basis.mem_as_filter_of_mem hs)
  exact ⟨s, hs', subset_rfl⟩
case mpr
α : Type u_1
f : Filter α
b : Basis α
⊢ f ≤ Basis.as_filter b → as_basis f ≤' b
no goals