no goals
α : Type u_1
β : Type ?u.81162
γ : Type ?u.81165
ι : Sort u_2
ι' : Sort ?u.81171
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
hl : HasBasis la pa sa
i j : ι
hi : pa i
hj : pa j
⊢ ∃ k, pa k ∧ sa k ⊆ sa i ∧ sa k ⊆ sa j
simpa only [exists_prop, subset_inter_iff] using
  hl.mem_iff.1 (inter_mem (hl.mem_of_mem hi) (hl.mem_of_mem hj))