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

State before:
⊢ ∀ (x : 𝕊), invHomeomorph.symm x = invHomeomorph x
Tactic:
simp only [invHomeomorph, Homeomorph.homeomorph_mk_coe_symm, invEquiv_symm,
  Homeomorph.homeomorph_mk_coe, eq_self_iff_true, forall_const]
State after:
no goals