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

State before:
x : 𝕊
⊢ ↑(extChartAt I ∞) x = x⁻¹.toComplex
Tactic:
simp only [extChartAt_inf, PartialEquiv.trans_apply, coePartialEquiv_symm_apply,
  Equiv.toPartialEquiv_apply, invEquiv_apply]
State after:
no goals