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

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

⊢ ∞⁻¹ = ∞ ↔ ∞ = 0

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

State before:
case h₁

⊢ ∞⁻¹ = ∞ ↔ ∞ = 0
Tactic:
simp only [inv_inf]
State after:
case h₁

⊢ 0 = ∞ ↔ ∞ = 0

State before:
case h₁

⊢ 0 = ∞ ↔ ∞ = 0
Tactic:
exact ⟨Eq.symm, Eq.symm⟩
State after:
no goals

State before:
case h₂
x✝ : ℂ
⊢ (↑x✝)⁻¹ = ∞ ↔ ↑x✝ = 0
Tactic:
simp only [inv_def, inv, not_not, imp_false, ite_eq_left_iff, OnePoint.coe_ne_infty]
State after:
no goals