no goals
X : Type u_2
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
α : Type u_1
f : OnePoint X → α
l : Filter α
⊢ Tendsto f (𝓝 ∞) l ↔ Tendsto f (pure ∞) l ∧ Tendsto (f ∘ some) (coclosedCompact X) l
simp [nhds_infty_eq, and_comm]