A smooth curve has a formal coordinate at every point

Choose a holomorphic chart $z$ centered at $p$, available by the smooth-curve hypothesis in [F1]. Then ${\mathfrak{m}}_p=(z)$. For each $k\ge 1$, the Taylor truncation map ${\mathcal{O}}_{X,p}\to \mathbb{C}[z]\mathrm{/}(z^k)$ is a surjective ring homomorphism: every polynomial of degree less than $k$ is a holomorphic germ, and [F2] says its kernel consists exactly of germs divisible by $z^k$, namely ${\mathfrak{m}}_p^k$. It therefore induces an isomorphism ${\mathcal{O}}_{X,p}\mathrm{/}{\mathfrak{m}}_p^k\cong \mathbb{C}[z]\mathrm{/}(z^k)$.

These isomorphisms commute with the quotient maps as $k$ increases. Their inverse limit is : a compatible family is exactly its sequence of Taylor coefficients, and a zero sequence has zero truncation at every $k$. Renaming $z$ as $t$ gives the required complete-local-ring isomorphism and hence a formal coordinate.