no goals
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
l : Filter β
inst✝ : NeBot l
c d : α
⊢ Tendsto (fun x => c) l (𝓝 d) ↔ c = d
simp_rw [Tendsto, Filter.map_const, pure_le_nhds_iff]