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

State before:
⊢ ContinuousOn OnePoint.toComplex {∞}ᶜ
Tactic:
intro z m
State after:
z : 𝕊
m : z ∈ {∞}ᶜ
⊢ ContinuousWithinAt OnePoint.toComplex {∞}ᶜ z

State before:
z : 𝕊
m : z ∈ {∞}ᶜ
⊢ ContinuousWithinAt OnePoint.toComplex {∞}ᶜ z
Tactic:
induction z using OnePoint.rec
State after:
case h₁
m : ∞ ∈ {∞}ᶜ
⊢ ContinuousWithinAt OnePoint.toComplex {∞}ᶜ ∞

case h₂
x✝ : ℂ
m : ↑x✝ ∈ {∞}ᶜ
⊢ ContinuousWithinAt OnePoint.toComplex {∞}ᶜ ↑x✝

State before:
case h₁
m : ∞ ∈ {∞}ᶜ
⊢ ContinuousWithinAt OnePoint.toComplex {∞}ᶜ ∞
Tactic:
simp only [mem_compl_iff, mem_singleton_iff, not_true] at m
State after:
no goals

State before:
case h₂
x✝ : ℂ
m : ↑x✝ ∈ {∞}ᶜ
⊢ ContinuousWithinAt OnePoint.toComplex {∞}ᶜ ↑x✝
Tactic:
exact continuousAt_toComplex.continuousWithinAt
State after:
no goals