Analytic inverse coordinates at the punctures

The inverse standard coordinate of a puncture is complex differentiable away from the origin.

theorem TauCeti.ThricePuncturedSphere.Puncture.differentiableAt_coordInv (q : Puncture) {w : ℂ} (hw : w ≠ 0) : DifferentiableAt ℂ q.coordInv w

The inverse puncture coordinate is complex differentiable at every nonzero point.