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

State before:
z : 𝕊
⊢ invEquiv z = z⁻¹
Tactic:
simp only [invEquiv, Equiv.coe_fn_mk]
State after:
no goals