no goals
α : Type u_3
β : Type u_1
γ : Type ?u.70535
ι : Sort ?u.70538
ι' : Sort u_2
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
hlb : HasBasis lb pb sb
⊢ Tendsto f la lb ↔ ∀ (i : ι'), pb i → ∀ᶠ (x : α) in la, f x ∈ sb i
simp only [Tendsto, hlb.ge_iff, mem_map', Filter.Eventually]