In a standard proof that any sequence-compact metric space $(X,d)$ has a (finite) $\varepsilon$-net, the approach is the following: Make a sequence $(x_n)$ such that $$ x_{n+1}\notin\bigcup_{i=1}^n B_\varepsilon(x_i) $$ for all $n$, where $B_r(y)$ is the open ball of radius $r > 0$ around $y\in X$. Then prove that $(x_n)$ has no convergent subsequence.
The question is: Can we be sure that we can choose such a sequence? It is obvious that we must somehow make use of the Axiom of Choice, but in my opinion, it is not at all obvious that you can use that axiom recursively like this.
You don’t even need the full axiom of choice for this argument: the axiom of dependent choice ($\mathsf{DC}$) is sufficient.
Given $\epsilon>0$, let $\Sigma$ be the set of all finite sequences $\sigma$ in $X$ such that if $\sigma=\langle x_0,\ldots,x_{n-1}\rangle$, then
$$x_k\notin\bigcup_{\ell<k}B_\epsilon(x_\ell)$$
for each $k<n$. Define a relation $R$ on $\Sigma$ by $\sigma\mathrel{R}\tau$ if and only if $\sigma$ is a proper initial segment of $\tau$ (equivalently, $\sigma\subsetneqq\tau$). $R$ is a total relation on $\Sigma$, so by $\mathsf{DC}$ there is a sequence $\langle\sigma_n:n\in\Bbb N\rangle$ in $\Sigma$ such that $\sigma_n\mathrel{R}\sigma_{n+1}$ for each $n\in\Bbb N$. Then $\bigcup_{n\in\Bbb N}\sigma_n$ is an infinite sequence $\langle x_k:k\in\Bbb N\rangle$ in $X$ such that $$x_k\notin\bigcup_{\ell<k}B_\epsilon(x_\ell)$$ for each $k\in\Bbb N$.
In fact it’s only when you need to make infinitely many arbitrary choices, recursively or otherwise, that you need any part of the axiom of choice: you can always make any finite number of arbitrary choices.