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

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → X
y : X
fi : Tendsto f atInf (𝓝 y)
⊢ ContinuousAt (fill f y) ∞
Tactic:
simp only [OnePoint.continuousAt_infty', lift_inf, Filter.coclosedCompact_eq_cocompact, ←
  atInf_eq_cocompact, Function.comp, fill_coe, fill_inf, fi]
State after:
no goals