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

State before:
⊢ invEquiv.symm = invEquiv
Tactic:
simp only [Equiv.ext_iff, invEquiv, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk, eq_self_iff_true,
  forall_const]
State after:
no goals