I'm going through a proof for the theorem:
If $X$ is a metric, then X is compact if and only if X is sequentially compact.
I have already posted this here. However this time I'm looking at the converse. The proof so far is this:
We prove the contrapositive. So suppose that $X$ is not compact. Then we want to show that $X$ is not sequentially compact.
Since $X$ is not compact, $\exists \mathcal{A}$, an open cover with no finite subcover. So we need to construct a sequence such that no subsequence converges. So for all $x \in X$, $\exists s \in (0,1], A \in \mathcal{A}$ such that $B(x, s) \subset A$. So for all $x \in X$, $\exists A \in \mathcal{A}$ such that $B(x, s(x)) \subset A$.
A particular remark has been made: "$s$, the radius of the ball, exists due to the axiom of choice". I've not worked with the axiom of choice explicitly so I don't understand why it's required here. Any light shed on this would be much appreciated.
You are correct that you don't really need the axiom of choice there. Namely, you can always resort to radii of the form $\frac1n$, or just enumerate the rationals and work with that enumeration to choose uniformly radii using that enumeration.
The axiom of choice is needed when you want to choose the actual sequence without a convergent subsequence.
Let us consider the canonical counterexample of a metric space which is not compact, but is sequentially compact. This is a model of $\sf ZF$ in which there is $D\subseteq\Bbb R$ which is infinite, but has no countably infinite subset. We can also assume that $D$ is unbounded (otherwise limit yourself to the interval $(\inf D,\sup D)$ instead).
It is not hard to check that $D$ is sequentially compact, if $x_n$ is a sequence from $D$ then it has to have at least one element appearing infinitely often (otherwise we can construct an injection from $\Bbb N$ into $D$), so there is a convergent subsequence. But $D$ is not compact, because compact sets are still closed in $\Bbb R$ and infinite closed sets have countably infinite subsets.
So to witness the incompactness of $D$ consider the open cover $\{(-\infty,q)\cap D\mid q\in\Bbb Q\}$. Now every $d\in D$ has some rational radius, $q_d$ such that $B(d,q_d)\cap D$ is a subset of some $(-\infty,q)$. We can even map to each $d\in D$ the least $q$ such that $(-\infty,q)\cap D$. And ideally now we would like to choose a sequence of points which will be spaced enough not to have a convergent subsequence, but we can't. This is exactly where we appeal to the axiom of choice.