no goals
α : Type u_1
β : Type ?u.14022
γ : Type ?u.14025
ι : Sort u_2
ι' : Sort ?u.14031
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l p s
i✝ j✝ : ι
hi : p i✝
hj : p j✝
⊢ ∃ k, p k ∧ s k ⊆ s i✝ ∩ s j✝
simpa only [h.mem_iff] using inter_mem (h.mem_of_mem hi) (h.mem_of_mem hj)