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

State before:
z : ℂ
⊢ extChartAt I ↑z = coePartialEquiv.symm
Tactic:
simp only [coePartialHomeomorph, extChartAt, PartialHomeomorph.extend, chartAt_coe,
  PartialHomeomorph.symm_toPartialEquiv, modelWithCornersSelf_partialEquiv,
  PartialEquiv.trans_refl]
State after:
no goals