no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.317835
ι : Sort x
f : α → β
a : Filter α
b : β
⊢ Tendsto f a (pure b) ↔ ∀ᶠ (x : α) in a, f x = b
simp only [Tendsto, le_pure_iff, mem_map', mem_singleton_iff, Filter.Eventually]