rw [← hbc] at hs'
case h
α : Type u_1
b✝ c✝ b c : Basis α
hbc : as_filter b = as_filter c
s : Set α
hs : s ∈ c
hs' : s ∈ as_filter c
⊢ ∃ t, t ∈ b ∧ t ⊆ s
case h
α : Type u_1
b✝ c✝ b c : Basis α
hbc : as_filter b = as_filter c
s : Set α
hs : s ∈ c
hs' : s ∈ as_filter b
⊢ ∃ t, t ∈ b ∧ t ⊆ s