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

State before:
z : 𝕊
⊢ z⁻¹.toComplex = z.toComplex⁻¹
Tactic:
induction' z using OnePoint.rec with z
State after:
case h₁

⊢ ∞⁻¹.toComplex = ∞.toComplex⁻¹

case h₂
z : ℂ
⊢ (↑z)⁻¹.toComplex = (↑z).toComplex⁻¹

State before:
case h₁

⊢ ∞⁻¹.toComplex = ∞.toComplex⁻¹
Tactic:
simp only [inv_inf, toComplex_zero, toComplex_inf, inv_zero', inv_zero, eq_self_iff_true]
State after:
no goals

State before:
case h₂
z : ℂ
⊢ (↑z)⁻¹.toComplex = (↑z).toComplex⁻¹
Tactic:
by_cases z0 : z = 0
State after:
case pos
z : ℂ
z0 : z = 0
⊢ (↑z)⁻¹.toComplex = (↑z).toComplex⁻¹

case neg
z : ℂ
z0 : ¬z = 0
⊢ (↑z)⁻¹.toComplex = (↑z).toComplex⁻¹

State before:
case pos
z : ℂ
z0 : z = 0
⊢ (↑z)⁻¹.toComplex = (↑z).toComplex⁻¹
Tactic:
simp only [z0, coe_zero, inv_zero', toComplex_inf, toComplex_zero, inv_zero]
State after:
no goals

State before:
case neg
z : ℂ
z0 : ¬z = 0
⊢ (↑z)⁻¹.toComplex = (↑z).toComplex⁻¹
Tactic:
simp only [z0, inv_coe, Ne, not_false_iff, toComplex_coe]
State after:
no goals