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

State before:
z : ℂ
z0 : z ≠ 0
⊢ (↑z)⁻¹ = ↑z⁻¹
Tactic:
simp only [inv_def, inv, z0, WithTop.coe_eq_zero, toComplex_coe, if_false, coe_eq_zero]
State after:
no goals