Theorem: RiemannSphere.coe_tendsto_inf (Ray/AnalyticManifold/RiemannSphere.lean)

State before:
⊢ Tendsto (fun z => ↑z) atInf (𝓝 ∞)
Tactic:
rw [Filter.tendsto_iff_comap, OnePoint.comap_coe_nhds_infty, Filter.coclosedCompact_eq_cocompact]
State after:
⊢ atInf ≤ Filter.cocompact ℂ

State before:
⊢ atInf ≤ Filter.cocompact ℂ
Tactic:
exact atInf_le_cocompact
State after:
no goals