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

State before:
⊢ ∞⁻¹ = 0
Tactic:
simp [inv_def, inv, inf_ne_zero]
State after:
no goals