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

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

⊢ ∞⁻¹ = 0 ↔ ∞ = ∞

case h₂
z : ℂ
⊢ (↑z)⁻¹ = 0 ↔ ↑z = ∞

State before:
case h₁

⊢ ∞⁻¹ = 0 ↔ ∞ = ∞
Tactic:
simp only [inv_inf, eq_self_iff_true]
State after:
no goals

State before:
case h₂
z : ℂ
⊢ (↑z)⁻¹ = 0 ↔ ↑z = ∞
Tactic:
simp only [inv_def, inv, toComplex_coe]
State after:
case h₂
z : ℂ
⊢ (if ↑z = 0 then ∞ else ↑z⁻¹) = 0 ↔ ↑z = ∞

State before:
case h₂
z : ℂ
⊢ (if ↑z = 0 then ∞ else ↑z⁻¹) = 0 ↔ ↑z = ∞
Tactic:
by_cases z0 : (z : 𝕊) = 0
State after:
case pos
z : ℂ
z0 : ↑z = 0
⊢ (if ↑z = 0 then ∞ else ↑z⁻¹) = 0 ↔ ↑z = ∞

case neg
z : ℂ
z0 : ¬↑z = 0
⊢ (if ↑z = 0 then ∞ else ↑z⁻¹) = 0 ↔ ↑z = ∞

State before:
case pos
z : ℂ
z0 : ↑z = 0
⊢ (if ↑z = 0 then ∞ else ↑z⁻¹) = 0 ↔ ↑z = ∞

case neg
z : ℂ
z0 : ¬↑z = 0
⊢ (if ↑z = 0 then ∞ else ↑z⁻¹) = 0 ↔ ↑z = ∞
Tactic:
simp only [if_pos, z0, inf_ne_zero, inf_ne_zero.symm]
State after:
case neg
z : ℂ
z0 : ¬↑z = 0
⊢ (if ↑z = 0 then ∞ else ↑z⁻¹) = 0 ↔ ↑z = ∞

State before:
case neg
z : ℂ
z0 : ¬↑z = 0
⊢ (if ↑z = 0 then ∞ else ↑z⁻¹) = 0 ↔ ↑z = ∞
Tactic:
simp only [if_neg z0, coe_ne_inf, iff_false_iff]
State after:
case neg
z : ℂ
z0 : ¬↑z = 0
⊢ ¬↑z⁻¹ = 0

State before:
case neg
z : ℂ
z0 : ¬↑z = 0
⊢ ¬↑z⁻¹ = 0
Tactic:
rw [coe_eq_zero, _root_.inv_eq_zero]
State after:
case neg
z : ℂ
z0 : ¬↑z = 0
⊢ ¬z = 0

State before:
case neg
z : ℂ
z0 : ¬↑z = 0
⊢ ¬z = 0
Tactic:
simpa only [coe_eq_zero] using z0
State after:
no goals