have ⟨u, hu⟩ := h t ht.1
α : Type u_1
b c : Basis α
h : ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
s : Set α
hs : s ∈ as_filter c
t : Set α
ht : t ∈ c ∧ t ⊆ s
⊢ s ∈ as_filter b
α : Type u_1
b c : Basis α
h : ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
s : Set α
hs : s ∈ as_filter c
t : Set α
ht : t ∈ c ∧ t ⊆ s
u : Set α
hu : u ∈ b ∧ u ⊆ t
⊢ s ∈ as_filter b