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

State before:
z : 𝕊
h : z ≠ ∞
⊢ ↑z.toComplex = z
Tactic:
induction z using OnePoint.rec
State after:
case h₁
h : ∞ ≠ ∞
⊢ ↑∞.toComplex = ∞

case h₂
x✝ : ℂ
h : ↑x✝ ≠ ∞
⊢ ↑(↑x✝).toComplex = ↑x✝

State before:
case h₁
h : ∞ ≠ ∞
⊢ ↑∞.toComplex = ∞
Tactic:
simp only [ne_eq, not_true_eq_false] at h
State after:
no goals

State before:
case h₂
x✝ : ℂ
h : ↑x✝ ≠ ∞
⊢ ↑(↑x✝).toComplex = ↑x✝
Tactic:
simp only [toComplex_coe]
State after:
no goals