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

State before:
⊢ extChartAt I 0 = coePartialEquiv.symm
Tactic:
simp only [← coe_zero, extChartAt_coe]
State after:
no goals