no goals
X : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
Y : Type u_1
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
⊢ Tendsto (f ∘ some) (coclosedCompact X) (𝓝 (f ∞)) ↔
    ∀ (s : Set Y), s ∈ 𝓝 (f ∞) → ∃ t, IsClosed t ∧ IsCompact t ∧ MapsTo (f ∘ some) (tᶜ) s
simp only [hasBasis_coclosedCompact.tendsto_left_iff, and_assoc]