no goals
α : Type u_1
β : Type u_3
γ : Type ?u.65267
ι : Sort u_2
ι' : Sort ?u.65273
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
f : α → β
hl : HasBasis l p s
t : Set β
⊢ t ∈ Filter.map f l ↔ ∃ i, p i ∧ f '' s i ⊆ t
simp only [mem_map, image_subset_iff, hl.mem_iff, preimage]