Lemma 15.19.21E3C9C96E314E

Proof. The neighborhoods can be chosen nested, with closures avoiding the other points of $S$. Every sequence of regular points converging to $s_ a$ is $d_0$-Cauchy: its tail lies in each prescribed neighborhood, whose punctured diameter tends to zero. Interleaving two such sequences shows that they define the same completion point, denoted by $\widehat s_ a$. Density of $Y^\circ $ guarantees the existence of these sequences.

For each prescribed positive diameter, remove sufficiently small neighborhoods of all the points of $S$. Their complement is a compact subset of $Y^\circ $ and hence is totally bounded for $d_0$. The removed punctured neighborhoods each have the prescribed small diameter. Thus $Y^\circ $ is totally bounded, and its completion is compact.

The points $\widehat s_ a$ are distinct from one another and from the regular points. To see this, fix $s_ a$ and a different point $y\in Y$. Choose an open neighborhood $V$ of $s_ a$ whose closure avoids $y$ and $S\setminus \{ s_ a\} $, and choose $W\Subset V$ containing $s_ a$. There is a smooth function $\chi $ on $Y^\circ $, equal to one on $W\setminus S$ and zero outside $V$, whose derivative has compact support in $Y^\circ $. Indeed the transition takes place in the compact regular set $\overline V\setminus W$, where smooth cutoffs exist. Therefore $|\mathrm{d}\chi |_{g_0}\leq C$ for some finite $C$. Integration along curves gives

The Lipschitz extension of $\chi $ to the completion has value one at $\widehat s_ a$ and zero at the regular point $y$, or at $\widehat s_ b$ if $y=s_ b$. This proves the assertion.

Define $\iota $ by the identity on the regular locus and by $\iota (s_ a)=\widehat s_ a$. The intrinsic distance induces the smooth topology at each regular point. At $s_ a$, adjoining $\widehat s_ a$ to a punctured neighborhood does not increase its diameter, so the diameter hypothesis proves continuity of $\iota $. Every completion point is represented by a Cauchy sequence in $Y^\circ $. Compact metrizability of $Y$ gives a subsequence converging topologically either to a regular point or to some $s_ a$; the preceding arguments give its metric limit. Hence $\iota $ is surjective as well as injective. A continuous bijection from compact $Y$ to Hausdorff $\widehat Y$ is a homeomorphism. $\square$