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

State before:
z : ℂ
⊢ ContinuousAt OnePoint.toComplex ↑z
Tactic:
simp only [OnePoint.continuousAt_coe, Function.comp, toComplex_coe]
State after:
z : ℂ
⊢ ContinuousAt (fun x => x) z

State before:
z : ℂ
⊢ ContinuousAt (fun x => x) z
Tactic:
exact continuousAt_id
State after:
no goals