I'd like to present a more modular proof. The key lemma (which I learnt from Christian Sattler) is that any set $X$ is a filtered colimit of finite sets. Indeed, let $I$ be the category of pairs $(n, f)$ with $n \in \mathbb N$ and $f : [n] \to X$, where a morphism $(n, f) \to (m, g)$ is a function $p : [n] \to [m]$ such that $f = g \circ p$. Since the category of finite sets has finite colimits, so does $I$, and so in particular $I$ is filtered. Now $X$ is the colimit $\mathop{\mathrm{colim}}_{(n,f) \in I} [n]$ in the obvious way.

The free abelian group functor $F$ commutes with colimits, being a left adjoint, so $FX \cong \mathop{\mathrm{colim}}_{(n,f) \in I} F[n]$. Moreover, the functor $U$ sending an abelian group to its underlying set commutes with filtered colimits, so $UFX \cong \mathop{\mathrm{colim}}_{(n,f) \in I} UF[n]$.

The unit maps $[n] \to UF[n]$ are injective since $[n]$ has decidable equality. Filtered colimits commute with pullbacks in sets, so they preserve monomorphisms. This means precisely that the unit map $X \to UFX$ is also injective, as needed.

If we look more closely at the characterisation of equality in a sequential colimit of sets, we obtain an explicit description of $UFX$ as in previous answers.

I'd like to present a more modular proof. The key lemma (which I learnt from Christian Sattler) is that any set $X$ is a filtered colimit of finite sets. Indeed, let $I$ be the category of pairs $(n, f)$ with $n \in \mathbb N$ and $f : [n] \to X$, where a morphism $(n, f) \to (m, g)$ is a function $p : [n] \to [m]$ such that $f = g \circ p$. Since the category of finite sets has finite colimits, so does $I$, and so in particular $I$ is filtered. Now $X$ is the colimit $\mathop{\mathrm{colim}}_{(n,f) \in I} [n]$ in the obvious way.

The free abelian group functor $F$ commutes with colimits, being a left adjoint, so $FX \cong \mathop{\mathrm{colim}}_{(n,f) \in I} F[n]$. Moreover, the functor $U$ sending an abelian group to its underlying set commutes with filtered colimits, so $UFX \cong \mathop{\mathrm{colim}}_{(n,f) \in I} UF[n]$.

The unit maps $[n] \to UF[n]$ are injective since $[n]$ has decidable equality. Filtered colimits commute with pullbacks in sets, so they preserve monomorphisms. This means precisely that the unit map $X \to UFX$ is also injective, as needed.

If we look more closely at the characterisation of equality in a filtered colimit of sets, we obtain an explicit description of $UFX$ as in previous answers.