[proofplan]
The proof identifies the tangent space to the regular level set as the kernel of the differential $dJ_x$. We then test the vector $dJ_x(v)\in\mathfrak g^*$ against every $\xi\in\mathfrak g$, which converts the kernel condition into the vanishing of the differentials of the component functions $J^\xi$. The moment map identity rewrites those scalar equations as symplectic orthogonality to all fundamental vector fields, and the orbit tangent description converts this into the symplectic orthogonal of $T_x(G\cdot x)$.
[/proofplan]
[step:Identify the tangent space to the regular level set with $\ker dJ_x$]
Fix $x\in J^{-1}(\mu)$. Since $\mu$ is a regular value of the smooth map $J:M\to\mathfrak g^*$, the regular level set theorem implies that $J^{-1}(\mu)$ is a smooth embedded submanifold of $M$ near $x$ and that
\begin{align*}
T_xJ^{-1}(\mu)=\ker dJ_x.
\end{align*}
Here we identify $T_{J(x)}\mathfrak g^*$ with $\mathfrak g^*$ by the translation identification of the tangent space of a [finite-dimensional vector space](/page/Finite-Dimensional%20Vector%20Space) with the [vector space](/page/Vector%20Space) itself.
[/step]
[step:Test the kernel condition against all elements of the Lie algebra]
For each $\xi\in\mathfrak g$, define the linear evaluation map $\operatorname{ev}_\xi:\mathfrak g^*\to\mathbb R$ by
\begin{align*}
\operatorname{ev}_\xi(\alpha)=\alpha(\xi)
\end{align*}
for every $\alpha\in\mathfrak g^*$. Then $J^\xi=\operatorname{ev}_\xi\circ J$. Since $\operatorname{ev}_\xi$ is linear, its differential at every point of $\mathfrak g^*$ is again $\operatorname{ev}_\xi$ under the vector-space tangent identification. Hence, for every $v\in T_xM$,
\begin{align*}
dJ^\xi_x(v)=d(\operatorname{ev}_\xi)_{J(x)}(dJ_x(v))=\operatorname{ev}_\xi(dJ_x(v))=dJ_x(v)(\xi).
\end{align*}
Therefore
\begin{align*}
v\in\ker dJ_x
\end{align*}
if and only if
\begin{align*}
dJ^\xi_x(v)=0
\end{align*}
for every $\xi\in\mathfrak g$.
[guided]
We want to understand the vector equation $dJ_x(v)=0$ in the dual vector space $\mathfrak g^*$. A covector in $\mathfrak g^*$ is zero exactly when it gives zero after evaluation on every element of $\mathfrak g$. For this reason, fix an arbitrary $\xi\in\mathfrak g$ and define the evaluation map $\operatorname{ev}_\xi:\mathfrak g^*\to\mathbb R$ by
\begin{align*}
\operatorname{ev}_\xi(\alpha)=\alpha(\xi)
\end{align*}
for every $\alpha\in\mathfrak g^*$.
The component function $J^\xi:M\to\mathbb R$ is precisely the composite $J^\xi=\operatorname{ev}_\xi\circ J$. Since $\operatorname{ev}_\xi$ is a [linear map](/page/Linear%20Map) between finite-dimensional vector spaces, its differential is the same linear map at every point after identifying tangent spaces to vector spaces by translation. Applying the chain rule to $J^\xi=\operatorname{ev}_\xi\circ J$ at the point $x$ gives, for every $v\in T_xM$,
\begin{align*}
dJ^\xi_x(v)=d(\operatorname{ev}_\xi)_{J(x)}(dJ_x(v))=\operatorname{ev}_\xi(dJ_x(v))=dJ_x(v)(\xi).
\end{align*}
Now $dJ_x(v)$ is an element of $\mathfrak g^*$. Thus $dJ_x(v)=0$ if and only if $dJ_x(v)(\xi)=0$ for every $\xi\in\mathfrak g$. By the displayed identity, this is equivalent to
\begin{align*}
dJ^\xi_x(v)=0
\end{align*}
for every $\xi\in\mathfrak g$. This converts the vector-valued kernel condition into scalar conditions for the component Hamiltonians $J^\xi$.
[/guided]
[/step]
[step:Use the moment map identity to obtain symplectic orthogonality to fundamental vector fields]
By the defining moment map identity, for every $\xi\in\mathfrak g$,
\begin{align*}
dJ^\xi=\iota_{\xi_M}\omega.
\end{align*}
Evaluating at $x$ and applying both sides to $v\in T_xM$ gives
\begin{align*}
dJ^\xi_x(v)=\omega_x(\xi_M(x),v).
\end{align*}
Since $\omega_x$ is skew-symmetric, this vanishing condition is equivalent to
\begin{align*}
\omega_x(v,\xi_M(x))=0.
\end{align*}
Combining this with the previous step and with $T_xJ^{-1}(\mu)=\ker dJ_x$ yields
\begin{align*}
T_xJ^{-1}(\mu)=\{v\in T_xM:\omega_x(v,\xi_M(x))=0\text{ for every }\xi\in\mathfrak g\}.
\end{align*}
[/step]
[step:Rewrite the condition as the symplectic orthogonal of the orbit tangent space]
Let $a_x:G\to M$ be the orbit map defined by
\begin{align*}
a_x(g)=g\cdot x.
\end{align*}
For $\xi\in\mathfrak g=T_eG$, the differential of $a_x$ at the identity element $e\in G$ satisfies
\begin{align*}
d(a_x)_e(\xi)=\left.\frac{d}{dt}\right|_{t=0}\exp(t\xi)\cdot x=\xi_M(x).
\end{align*}
The standard orbit tangent description for smooth Lie group actions gives
\begin{align*}
T_x(G\cdot x)=\{d(a_x)_e(\xi):\xi\in\mathfrak g\}=\{\xi_M(x):\xi\in\mathfrak g\}.
\end{align*}
By definition, the symplectic orthogonal of $T_x(G\cdot x)\subset T_xM$ is
\begin{align*}
(T_x(G\cdot x))^\omega=\{v\in T_xM:\omega_x(v,w)=0\text{ for every }w\in T_x(G\cdot x)\}.
\end{align*}
Substituting $T_x(G\cdot x)=\{\xi_M(x):\xi\in\mathfrak g\}$ into this definition gives
\begin{align*}
(T_x(G\cdot x))^\omega=\{v\in T_xM:\omega_x(v,\xi_M(x))=0\text{ for every }\xi\in\mathfrak g\}.
\end{align*}
Together with the previous step, this proves
\begin{align*}
T_xJ^{-1}(\mu)=(T_x(G\cdot x))^\omega.
\end{align*}
[/step]
