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

State before:
z : 𝕊
⊢ invHomeomorph z = z⁻¹
Tactic:
simp only [invHomeomorph, Homeomorph.homeomorph_mk_coe, invEquiv_apply]
State after:
no goals