= Solution
Choose affine neighborhoods $U_0=\operatorname{Spec}A$ of $x$ and $V_0=\operatorname{Spec}B$ of $y$, and orient the given <local ring> isomorphism as
$$
\alpha:B_{\mathfrak m_y}\longrightarrow A_{\mathfrak m_x}.
$$
Both algebras are finitely presented over $k$. Choose finitely many generators of $B$. Their images under $\alpha$ are fractions in $A$ whose denominators do not vanish at $x$. After inverting the product of those denominators, they define <regular functions> on an affine open neighborhood of $x$. The finitely many defining relations of $B$ vanish as germs at $x$; each vanishes on a further open neighborhood. Shrinking finitely many times therefore turns those fractions into an actual algebra homomorphism $B\to\mathcal O(U_1)$, and hence a <morphism of algebraic varieties> $F:U_1\to V_0$ inducing $\alpha$ on the <local rings>.
A local-ring isomorphism preserves the <maximal ideal>. Its induced residue-field map is the identity of $k$, because it is a $k$-algebra map. Evaluating every coordinate generator consequently shows $F(x)=y$. Apply the identical finite-generator and finite-relation construction to $\alpha^{-1}$ to obtain $G:V_1\to U_0$ with $G(y)=x$.
On $U_2=U_1\cap F^{-1}(V_1)$ the composition $GF$ is defined, and on $V_2=V_1\cap G^{-1}(U_1)$ the composition $FG$ is defined. Their maps on <local rings> are the identities. Thus the coordinate differences between $GF$ and the identity vanish as germs at $x$; finitely many coordinate generators allow us to shrink to $U_3\subseteq U_2$ on which $GF$ actually is the identity. Likewise shrink to $V_3\subseteq V_2$ on which $FG$ is the identity. Finally take
$$
U=U_3\cap F^{-1}(V_3),\qquad V=V_3\cap G^{-1}(U_3).
$$
These are open neighborhoods of the specified points. If $u\in U$, then $F(u)\in V_3$ and $G(F(u))=u\in U_3$, so $F(u)\in V$. Conversely, if $v\in V$, then $G(v)\in U_3$ and $F(G(v))=v\in V_3$, so $G(v)\in U$. Therefore the restrictions are mutual inverse regular maps, proving
$$
\boxed{F:U\xrightarrow{\ \sim\ }V,\qquad F(x)=y.}
$$
This proves <isomorphic local rings determine isomorphic neighborhoods> using actual <regular functions> and finite presentations. The conclusion concerns neighborhood isomorphisms, rather than just isomorphisms of formal completions.
Back to article page