The diagonal of a smooth manifold is a closed embedded submanifold

The diagonal map $\delta$ is smooth: by [F3] applied to $\delta$ it suffices that its two components ${\pi }_1\circ \delta$ and ${\pi }_2\circ \delta$ are smooth, and both components equal ${\mathrm{i}\mathrm{d}}_X$, which is smooth by [F4].

The map $\delta$ is injective: if $(x,x)=(y,y)$ then reading the first coordinate gives $x=y$. Its image is ${\mathrm{\Delta }}_X$ by the definition of ${\mathrm{\Delta }}_X$, and ${\mathrm{\Delta }}_X$ carries the subspace topology by [L1] and [F5].

The projection ${\pi }_1:X\times X\to X$ is smooth: in a product chart $(\phi \times \phi )$ of [F2] its coordinate representative is the Euclidean projection $(u,v)\mapsto u$, which is smooth, and smoothness is a local condition on the source.

The restricted slice charts of ${\mathrm{\Delta }}_X$ are smoothly compatible and generate the subspace topology by [L2] and [F5]; this is the canonical smooth structure on ${\mathrm{\Delta }}_X$ announced in the statement, and it is the structure used in the remaining steps.

The differential of $\delta$ is injective at every point: by [L7] applied to ${\pi }_1\circ \delta ={\mathrm{i}\mathrm{d}}_X$, the identity $d({\pi }_1\circ \delta {)}_x=d({\pi }_1{)}_{\delta (x)}\circ d{\delta }_x$ holds, while the defining formula [L8] gives $d({\mathrm{i}\mathrm{d}}_X{)}_x={\mathrm{i}\mathrm{d}}_{T_{x}X}$ because $g\circ {\mathrm{i}\mathrm{d}}_X=g$ for every germ $g$. Hence $d{\pi }_1\circ d{\delta }_x={\mathrm{i}\mathrm{d}}_{T_{x}X}$, so $d{\delta }_x$ is injective and $\delta$ is an immersion.

For this structure the corestriction ${\delta }^0:X\to {\mathrm{\Delta }}_X$ is smooth, because its ambient composite with the inclusion ${\mathrm{\Delta }}_X\hookrightarrow X\times X$ is $\delta$, which is smooth by step 1.1; this is the criterion of [L9].

The inverse ${\pi }_1{\mathrm{\mid }}_{{\mathrm{\Delta }}_X}$ is smooth by the ambient-extension criterion of [L10], applied with the ambient map ${\pi }_1$, which is smooth by step 1.3 and restricts to ${\pi }_1{\mathrm{\mid }}_{{\mathrm{\Delta }}_X}$ on ${\mathrm{\Delta }}_X$.

The map $\delta$ is continuous by [L6] and step 1.1, and the restriction ${\pi }_1{\mathrm{\mid }}_{{\mathrm{\Delta }}_X}:{\mathrm{\Delta }}_X\to X$ is continuous as the restriction of the continuous projection ${\pi }_1$ of [L5] to the subspace ${\mathrm{\Delta }}_X$. The two maps are mutually inverse bijections between $X$ and ${\mathrm{\Delta }}_X$, because ${\pi }_1(x,x)=x$ and $\delta ({\pi }_1(x,x))=(x,x)$ for every $x\in X$. Hence the corestriction of $\delta$ to ${\mathrm{\Delta }}_X$ is a homeomorphism, so $\delta$ is a smooth embedding onto ${\mathrm{\Delta }}_X$ by [L3] and [L4], completing the first two claims.

By steps 2.2 and 2.3 the corestriction ${\delta }^0$ is a bijective smooth map with smooth inverse, hence a diffeomorphism onto ${\mathrm{\Delta }}_X$ in the canonical structure of step 1.4; this is the final claim.

Finally ${\mathrm{\Delta }}_X$ is closed in $X\times X$: given $(x,y)\mathrm{\notin }{\mathrm{\Delta }}_X$ one has $x\mathrm{\ne }y$, and since $X$ is Hausdorff by [F1] there are disjoint open sets $U\ni x$ and $V\ni y$; then $U\times V$ is a basis open set of [L5] containing $(x,y)$ and disjoint from ${\mathrm{\Delta }}_X$, because a point of $U\times V$ would have equal coordinates in $U\cap V=\mathrm{\varnothing }$. So the complement of ${\mathrm{\Delta }}_X$ is open, and ${\mathrm{\Delta }}_X$ is closed.