no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.317172
ι : Sort x
f : α → β
l : Filter α
s : Set β
⊢ Tendsto f l (𝓟 s) ↔ ∀ᶠ (a : α) in l, f a ∈ s
simp only [Tendsto, le_principal_iff, mem_map', Filter.Eventually]