A trick to avoid choice in proper metrization of countable disjoint union of proper metric spaces A proper metric space is a metric space where closed balls are compact. Equivalently, it's a metric space such that bounded sets are compact.
In this answer user Saucy O'Path describes, given a countable sequence $\{(X_j,d_j)\}_{j\in\Bbb N}$ of (non-empty) proper metric spaces, a proper metric on $\coprod_{j\in\Bbb N} X_j$ such that the natural embeddings are isometries.
The answer is (perhaps unnecessarily) lengthy, but long story short the geometric idea is that there is a building $B$ where the $n$-th floor is $(X_n,d_n)$ and there is one staircase connecting all the floors at distance $1$ each from the next. The disjoint union is seen as the subspace you obtain by removing the staircase. However, for each floor $X_n$ we must keep track of the point $x_n$ where the door to the staircase used to be, so that the distance is $$d((a,n),(b,m))=\begin{cases}d_n(a,b)&\text{if }n=m\\ d_n(a,x_n)+\lvert n-m\rvert+d_m(b,x_m)&\text{if }n\ne m\end{cases}$$
for some sequence $\{x_k\}_{k\in\Bbb N}$ such that $x_k\in X_k$.

Question: This construction metrizes the topological space $\coprod_{j\in\Bbb N}X_j$ with a proper metric $d$ such that the canonical embeddings $(X_k,d_k)\hookrightarrow \left(\prod_{j\in\Bbb N}X_j,d\right)$ are isometries. However, it uses countable choice. Is there a construction that achieves the same goal while avoiding countable choice?

 A: There is no such construction in ZF (assuming ZF is consistent).
As Milo Brandt noted in the comments, the statement that it's always possible to add a (proper) metric to the disjoint union with isometries on every component is equivalent to asking that for every countable sequence of non-empty proper metric spaces $(X_i,d_i)$ one can construct a sequence of non-empty compact sets $C_i\subseteq X_i.$
Let $\mathcal P(\mathbb N)$ denote the powerset of the set of naturals. Let $a\sim b$ mean that the symmetric difference $a\triangle b$ is finite. I claim that it is consistent with ZF that the following statement "(V)" holds.

(V) There is a countable sequence of equivalence classes $X_1,X_2,\dots\in \mathcal{P}(\mathbb N)/\sim$ with no choice function.

Each equivalence class $X_i$ can be given a proper metric space structure by $d(a,b)=\sum_{i\in a\triangle b} i.$ (Assuming the convention $0\not\in\mathbb N.$) A non-empty compact subset has a minimum element in lexicographic order. So a sequence of choices of non-empty compact sets $C_i\subset X_i$ would give a choice function for the sequence $X_i,$ contradicting (V).
To construct a suitable model of ZF, I don't know a standard example so you need to dive into set theory. I think it's a straightforward modification of standard techniques but needs a lot of background, and I'm just going to give a sketch. I suggest modifying the construction in Jech, Set Theory, 3rd Millenium Ed, Example 15.59. Given a transitive model $M$ of ZFC this produces a model $N\supset M$ with nice properties (every ultrafilter on $\omega$ is principal).
Instead of taking symmetries to be arbitrary sets $X\subset\omega\times\omega$ in $M,$ take only the $X$ such that $\{m : (n,m)\in X\}$ is finite for each $n.$
The symmetric model $N$ will contain the Cohen reals $\dot{a_i}$ and the sequence of $\sim$-equivalence classes $[\dot{a_1}],[\dot{a_2}],\dots,$ but no choice function for this sequence.
