no goals
α : Type u_1
β : Type u_3
γ : Type ?u.70952
ι : Sort u_2
ι' : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
hla : HasBasis la pa sa
hlb : HasBasis lb pb sb
⊢ Tendsto f la lb ↔ ∀ (ib : ι'), pb ib → ∃ ia, pa ia ∧ ∀ (x : α), x ∈ sa ia → f x ∈ sb ib
simp [hlb.tendsto_right_iff, hla.eventually_iff]