have hs' := h s (Basis.mem_as_filter_of_mem hs)
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
s : Set α
hs : s ∈ b
⊢ ∃ t, t ∈ as_basis f ∧ t ⊆ s
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
s : Set α
hs : s ∈ b
hs' : s ∈ f
⊢ ∃ t, t ∈ as_basis f ∧ t ⊆ s