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 (pure ∞) l ∧ Tendsto (f ∘ some) (coclosedCompact X) l ↔
    ∀ (s : Set α), s ∈ l → f ∞ ∈ s ∧ ∃ t, IsClosed t ∧ IsCompact t ∧ MapsTo (f ∘ some) (tᶜ) s
simp only [tendsto_pure_left, hasBasis_coclosedCompact.tendsto_left_iff, forall_and,
  and_assoc, exists_prop]