Every smooth manifold admits a smooth proper exhaustion function

If $M=\mathrm{\varnothing }$, the empty function has all the stated properties. Otherwise form the set of all relatively compact smooth coordinate-ball tuples, including their chart data. Their balls cover $M$ by [F1]. Fix a countable basis. For each nonempty basis member contained in an eligible ball, [A1] selects one such tuple. The selected balls cover $M$, since every point lies in a basis member contained in an eligible ball. Enumerate them as $(B_n{)}_{n\ge 1}$, repeating one if the nonempty selected family is finite. This uses countably many choices, not a choice at every point.

Put $H_r={\bigcup }_{n\le r}\overline{B_n}$. By [L1], these are compact and closed, and their interiors form an increasing open cover of $M$. Set $r_1=1$ and recursively let $r_{m+1}$ be the least integer greater than $r_m$ satisfying $H_{r_m}\subseteq \mathrm{int}{H}_{r_{m+1}}$. Compactness gives such an integer by taking a finite subcover of $H_{r_m}$ from the increasing interiors. For $K_m=H_{r_m}$, one has $K_m\subseteq \mathrm{int}{K}_{m+1},M={\bigcup }_{m\ge 1}\mathrm{int}{K}_m\mathrm{.}$ The recursion is by least integers and needs no dependent choice.

For each $n\ge 1$, the set of smooth cutoffs ${\chi }_n:M\to [0,1]$ equal to one near $K_n$ and supported in $\mathrm{int}{K}_{n+1}$ is nonempty by [L2]. Use [A1] to choose one cutoff for each $n$. Put $g_n=1-{\chi }_n$, a smooth nonnegative function by [L4].

The support family $(\mathrm{supp}{g}_n)$ is locally finite, not merely pointwise finite. Indeed, for $x\in \mathrm{int}{K}_t$ and every $n\ge t$, one has $\mathrm{int}{K}_t\subseteq K_n$, so ${\chi }_n=1$ on that whole open set. Thus $g_n$ vanishes there and its support misses $\mathrm{int}{K}_t$. This neighbourhood meets at most the supports with $n<t$. Hence $h={\sum }_{n\ge 1}{g}_n$ is smooth, continuous and nonnegative by [L3].

Let $c\ge 0$ and choose an integer $N>c$. If $x\mathrm{\notin }{K}_{N+1}$, then for each $1\le n\le N$ the support of ${\chi }_n$ is contained in $K_{n+1}\subseteq K_{N+1}$, so ${\chi }_n(x)=0$ and $g_n(x)=1$. Consequently $h(x)\ge N>c$. Thus $\{x:h(x)\le c\}\subseteq K_{N+1}\mathrm{.}$ This sublevel set is closed by continuity of $h$, hence compact by [L1]. For $c<0$ it is empty and therefore compact.

Finally let $C\subseteq [0,\mathrm{\infty })$ be compact. It is closed by [L1], and the increasing open cover $([0,n){)}_{n\ge 1}$ of $[0,\mathrm{\infty })$ gives an integer $N$ with $C\subseteq [0,N]$ by a finite subcover. Therefore $h^{-1}(C)$ is a closed subset of the compact sublevel set $\{h\le N\}$, hence compact by [L1]. Together with the empty case, this proves properness and the stated exhaustion properties.