A complete, totally bounded metric space is compact, proved from countable choice used exactly once

Suppose $(X,d)$ is complete and totally bounded and that some family $\mathcal{U}$ of open subsets of $X$ with union $X$ has no finite subfamily with union $X$; call a subset $S \subseteq X$ finitely covered when some finite subfamily of $\mathcal{U}$ has union containing $S$, so that $X$ itself is not finitely covered.

$X \ne \emptyset$, since the empty subfamily of $\mathcal{U}$ has union $\emptyset$ and would finitely cover an empty $X$; consequently, for each $n \in \mathbb{N}$, the set $E_n$ of pairs $(m,f)$ with $m \in \mathbb{N}$ and $f : \sigma(m) \to X$ such that $\{f(0), \dots, f(m)\}$ is a finite $1/(n+1)$-net for $X$ is nonempty.

Countable choice applied to $(E_n)_{n \in \mathbb{N}}$ fixes, once and for all, a function $n \mapsto (m_n, f_n)$ with $(m_n,f_n) \in E_n$; this is the single appeal to a choice principle in this proof, and the family $(E_n)$ was written down at step 2.1 before any of it was made.

If $S \subseteq X$ is not finitely covered and $n \in \mathbb{N}$, then $S \cap B(f_n(i), 1/(n+1))$ fails to be finitely covered for at least one $i \le m_n$: otherwise finite choice applied to $i \mapsto \{\text{finite subfamilies of } \mathcal{U} \text{ covering } S \cap B(f_n(i), 1/(n+1))\}$ produces one such subfamily for each $i \le m_n$, and the concatenation of those finitely many finite lists is a finite subfamily of $\mathcal{U}$ whose union contains $S = \bigcup_{i \le m_n} \big(S \cap B(f_n(i), 1/(n+1))\big)$.

Let $i(n,S)$ be the least $i \le m_n$ with $S \cap B(f_n(i), 1/(n+1))$ not finitely covered when such an $i$ exists, and $0$ otherwise; recursion on $\mathbb{N} \times \mathcal{P}(X)$ with starting value $(0, X)$ and rule $F(n,S) := \big(n+1,\ S \cap B(f_n(i(n,S)), 1/(n+1))\big)$ then produces $g : \mathbb{N} \to \mathbb{N} \times \mathcal{P}(X)$ whose first coordinate at $n$ is $n$; write $A_n$ for its second coordinate and $c_n := f_n(i(n,A_n))$.

By induction, no $A_n$ is finitely covered: $A_0 = X$ is not, by step 1.1, and if $A_n$ is not then step 4.1 supplies an admissible $i$, so $i(n,A_n)$ is one and $A_{n+1} = A_n \cap B(c_n, 1/(n+1))$ is not finitely covered either. In particular every $A_n$ is nonempty, since the empty set is finitely covered by the empty subfamily; moreover $A_{n+1} \subseteq A_n$ and $A_{n+1} \subseteq B(c_n, 1/(n+1))$.

The sequence $(c_n)$ is Cauchy: for $m \ge n$ one has $A_{m+1} \subseteq A_{n+1} \subseteq B(c_n, 1/(n+1))$ and $A_{m+1} \subseteq B(c_m, 1/(m+1))$, and taking $z \in A_{m+1}$ gives $d(c_n,c_m) \le d(c_n,z) + d(z,c_m) < 1/(n+1) + 1/(m+1) \le 2/(n+1)$; so given a rational $\eta > 0$, a natural $N \ge 1$ with $1/N < \eta/2$ makes $d(c_n,c_m) < \eta$ for all $n,m \ge N$.

By completeness $c_n \to p$ for some $p \in X$; since $\mathcal{U}$ has union $X$ there is $U \in \mathcal{U}$ with $p \in U$, and openness of $U$ gives a real $r > 0$ with $B(p,r) \subseteq U$.

Take a natural $N \ge 1$ with $1/N < r/2$, then $K \in \mathbb{N}$ with $d(c_n,p) < 1/N$ for all $n \ge K$, and let $n$ be whichever of $N$ and $K$ is the greater; then $1/(n+1) < 1/N < r/2$ and $d(c_n,p) < r/2$, so every $y \in A_{n+1} \subseteq B(c_n,1/(n+1))$ satisfies $d(y,p) \le d(y,c_n) + d(c_n,p) < r$, that is $A_{n+1} \subseteq B(p,r) \subseteq U$.

So the one-member subfamily $\{U\}$ of $\mathcal{U}$ has union containing $A_{n+1}$, making $A_{n+1}$ finitely covered and contradicting step 6.1; the assumption of step 1.1 therefore fails, every family of open sets with union $X$ has a finite subfamily with union $X$, and $(X,d)$ is compact.