[proofplan]
The proof follows the five constructions in the statement. First, $G$-invariance of $H$ and the moment-map identity imply that every component $J^\xi$ is constant along $X_H$, so $X_H$ is tangent to the moment level $Z=J^{-1}(\mu)$. Next, symplecticity of the action and invariance of $H$ imply that $X_H|_Z$ is $G_\mu$-invariant, hence descends through the principal quotient $\pi:Z\to M_\mu$. The invariant Hamiltonian also factors uniquely through the quotient, and the identity $\pi^*\omega_\mu=i^*\omega$ then identifies the descended vector field with $X_{H_\mu}$; applying the chain rule projects integral curves to integral curves.
[/proofplan]
[step:Use invariance of $H$ to prove conservation of the moment map]
For $\xi\in\mathfrak g$, define
\begin{align*}
J^\xi:M\to\mathbb R,\qquad p\mapsto J(p)(\xi).
\end{align*}
Let $\xi_M\in\mathfrak X(M)$ be the fundamental vector field generated by $\xi$. Since $H$ is $G$-invariant, differentiating the identity
\begin{align*}
H(\exp(s\xi)\cdot p)=H(p)
\end{align*}
at $s=0$ gives
\begin{align*}
dH_p((\xi_M)_p)=0
\end{align*}
for every $p\in M$. Using $\iota_{X_H}\omega=dH$, this becomes
\begin{align*}
\omega_p((X_H)_p,(\xi_M)_p)=0.
\end{align*}
By skew-symmetry of $\omega$ and by the moment-map convention $dJ^\xi=\iota_{\xi_M}\omega$, we obtain
\begin{align*}
dJ^\xi_p((X_H)_p)=\omega_p((\xi_M)_p,(X_H)_p)=0.
\end{align*}
Since this holds for every $\xi\in\mathfrak g$, the covector $dJ_p((X_H)_p)\in\mathfrak g^*$ is zero. Thus $X_H$ is tangent to every level set of $J$, in particular to $Z=J^{-1}(\mu)$.
[guided]
Fix $\xi\in\mathfrak g$, and define the real-valued component of the moment map by
\begin{align*}
J^\xi:M\to\mathbb R,\qquad p\mapsto J(p)(\xi).
\end{align*}
The goal is to show that $J^\xi$ does not change along the Hamiltonian vector field $X_H$. Since the components $J^\xi$ separate the values of $J$ as $\xi$ varies through $\mathfrak g$, this will imply that the full moment map $J$ is constant along the flow.
Let $\xi_M\in\mathfrak X(M)$ be the fundamental vector field generated by $\xi$. Because $H$ is $G$-invariant, for every $p\in M$ and every $s$ for which $\exp(s\xi)$ is defined, we have
\begin{align*}
H(\exp(s\xi)\cdot p)=H(p).
\end{align*}
Differentiating this identity at $s=0$ gives
\begin{align*}
dH_p((\xi_M)_p)=0.
\end{align*}
Now use the defining equation for the Hamiltonian vector field:
\begin{align*}
\iota_{X_H}\omega=dH.
\end{align*}
Evaluating this one-form on $(\xi_M)_p$ gives
\begin{align*}
dH_p((\xi_M)_p)=\omega_p((X_H)_p,(\xi_M)_p).
\end{align*}
Therefore
\begin{align*}
\omega_p((X_H)_p,(\xi_M)_p)=0.
\end{align*}
The moment-map convention is
\begin{align*}
dJ^\xi=\iota_{\xi_M}\omega.
\end{align*}
Evaluating this identity on $(X_H)_p$ gives
\begin{align*}
dJ^\xi_p((X_H)_p)=\omega_p((\xi_M)_p,(X_H)_p).
\end{align*}
By skew-symmetry of $\omega_p$,
\begin{align*}
\omega_p((\xi_M)_p,(X_H)_p)=-\omega_p((X_H)_p,(\xi_M)_p)=0.
\end{align*}
Hence
\begin{align*}
dJ^\xi_p((X_H)_p)=0
\end{align*}
for every $\xi\in\mathfrak g$ and every $p\in M$.
Finally, for fixed $p\in M$, the vector $dJ_p((X_H)_p)\in\mathfrak g^*$ is determined by its pairings with all $\xi\in\mathfrak g$. Those pairings are exactly
\begin{align*}
dJ_p((X_H)_p)(\xi)=dJ^\xi_p((X_H)_p)=0.
\end{align*}
Thus $dJ_p((X_H)_p)=0$. Since $Z=J^{-1}(\mu)$ is a regular level set, its tangent space is
\begin{align*}
T_pZ=\ker dJ_p
\end{align*}
for every $p\in Z$. Therefore $(X_H)_p\in T_pZ$ for every $p\in Z$, so $X_H$ is tangent to $Z$.
[/guided]
[/step]
[step:Descend the Hamiltonian vector field to the quotient]
Let $X_Z\in\mathfrak X(Z)$ denote the restriction of $X_H$ to $Z$, meaning
\begin{align*}
di_p((X_Z)_p)=(X_H)_p
\end{align*}
for every $p\in Z$. This is well-defined because $X_H$ is tangent to $Z$.
For $g\in G$, let
\begin{align*}
\Phi_g:M\to M,\qquad p\mapsto g\cdot p
\end{align*}
be the action diffeomorphism. If $g\in G_\mu$, equivariance of $J$ gives $J(\Phi_g(p))=\operatorname{Ad}^*_g(J(p))=\mu$ for every $p\in Z$, where $\operatorname{Ad}^*$ is the coadjoint action defined in the statement. Thus $\Phi_g$ restricts to a diffeomorphism $Z\to Z$. Since $\Phi_g^*\omega=\omega$ and $H\circ\Phi_g=H$, we verify the Hamiltonian equation for $(\Phi_g)_*X_H$ by pulling back along $\Phi_g$. For every $p\in M$ and $v\in T_pM$,
\begin{align*}
(\Phi_g^*(\iota_{(\Phi_g)_*X_H}\omega))_p(v)=\omega_{\Phi_g(p)}(d\Phi_g((X_H)_p),d\Phi_g(v)).
\end{align*}
Because $\Phi_g^*\omega=\omega$, this equals
\begin{align*}
\omega_p((X_H)_p,v)=dH_p(v).
\end{align*}
Since $H\circ\Phi_g=H$, we also have $\Phi_g^*dH=dH$. Therefore $(\Phi_g)_*X_H$ satisfies
\begin{align*}
\iota_{(\Phi_g)_*X_H}\omega=dH.
\end{align*}
By nondegeneracy of $\omega$, $(\Phi_g)_*X_H=X_H$. In particular, for every $g\in G_\mu$, the restriction $X_Z$ is $G_\mu$-invariant on $Z$. Since the free proper action makes $\pi:Z\to M_\mu$ a smooth principal $G_\mu$-bundle, $\pi$ is a surjective submersion and its fibres are exactly the $G_\mu$-orbits. The vector-field descent theorem for principal quotients applies to the $G_\mu$-invariant smooth vector field $X_Z$ and gives a unique smooth vector field
\begin{align*}
Y_\mu\in\mathfrak X(M_\mu)
\end{align*}
such that
\begin{align*}
d\pi_p((X_Z)_p)=(Y_\mu)_{\pi(p)}
\end{align*}
for every $p\in Z$.
[guided]
The point of this step is to show that the vector field on the level set does not depend on the representative chosen in a $G_\mu$-orbit. For $g\in G_\mu$, equivariance of $J$ gives $J(g\cdot p)=\operatorname{Ad}^*_g(J(p))=\operatorname{Ad}^*_g\mu=\mu$ for every $p\in Z$, so the action diffeomorphism $\Phi_g:M\to M$ restricts to a diffeomorphism $Z\to Z$.
We next check invariance of the Hamiltonian vector field. Since $\Phi_g$ is symplectic and $H\circ\Phi_g=H$, pulling back the one-form $\iota_{(\Phi_g)_*X_H}\omega$ gives
\begin{align*}
\Phi_g^*(\iota_{(\Phi_g)_*X_H}\omega)=\iota_{X_H}(\Phi_g^*\omega)=\iota_{X_H}\omega=dH=\Phi_g^*dH.
\end{align*}
Because $\Phi_g$ is a diffeomorphism, pullback by $\Phi_g$ is injective on one-forms, hence $\iota_{(\Phi_g)_*X_H}\omega=dH$. The Hamiltonian vector field solving $\iota_X\omega=dH$ is unique by nondegeneracy of $\omega$, so $(\Phi_g)_*X_H=X_H$.
Restricting to $Z$, this says that $X_Z$ is invariant under every element of $G_\mu$. The quotient hypotheses say precisely that $\pi:Z\to M_\mu$ is a smooth principal $G_\mu$-bundle: it is a surjective submersion, and its fibres are the $G_\mu$-orbits. Therefore the vector-field descent theorem for principal quotients applies and produces a unique smooth vector field $Y_\mu\in\mathfrak X(M_\mu)$ satisfying
\begin{align*}
d\pi_p((X_Z)_p)=(Y_\mu)_{\pi(p)}
\end{align*}
for every $p\in Z$.
[/guided]
[/step]
[step:Descend the invariant Hamiltonian to the reduced space]
Since $H$ is $G$-invariant, its restriction
\begin{align*}
H|_Z:Z\to\mathbb R
\end{align*}
is constant on the $G_\mu$-orbits in $Z$. Because $\pi:Z\to M_\mu$ is the smooth quotient projection for the free proper $G_\mu$-action, it is a surjective submersion whose fibres are the $G_\mu$-orbits. The smooth factorization theorem for orbit-constant functions on a quotient applies to $H|_Z$ and gives a unique smooth function
\begin{align*}
H_\mu:M_\mu\to\mathbb R
\end{align*}
such that
\begin{align*}
H|_Z=\pi^*H_\mu.
\end{align*}
Equivalently,
\begin{align*}
H_\mu(\pi(p))=H(p)
\end{align*}
for every $p\in Z$.
[guided]
The restriction $H|_Z:Z\to\mathbb R$ is constant on each quotient fibre. Indeed, if $q=g\cdot p$ for some $g\in G_\mu$ and $p,q\in Z$, then $H(q)=H(g\cdot p)=H(p)$ by $G$-invariance of $H$. Since the fibres of $\pi:Z\to M_\mu$ are exactly the $G_\mu$-orbits, this means that $H|_Z$ is constant on the fibres of $\pi$.
The quotient factorization theorem for smooth functions now applies: $\pi$ is the smooth quotient projection of a free proper action, so a smooth function on $Z$ that is constant on the fibres of $\pi$ factors uniquely through a smooth function on $M_\mu$. Thus there is a unique smooth map $H_\mu:M_\mu\to\mathbb R$ satisfying
\begin{align*}
H|_Z=\pi^*H_\mu.
\end{align*}
Equivalently, $H_\mu(\pi(p))=H(p)$ for every $p\in Z$.
[/guided]
[/step]
[step:Identify the descended vector field with the reduced Hamiltonian vector field]
We prove that
\begin{align*}
\iota_{Y_\mu}\omega_\mu=dH_\mu.
\end{align*}
It suffices to pull back both sides by the surjective submersion $\pi:Z\to M_\mu$.
Let $p\in Z$ and let $v\in T_pZ$. Using $\pi^*\omega_\mu=i^*\omega$ and the defining relation $d\pi_p((X_Z)_p)=(Y_\mu)_{\pi(p)}$, we compute
\begin{align*}
(\pi^*(\iota_{Y_\mu}\omega_\mu))_p(v)=\omega_{\mu,\pi(p)}((Y_\mu)_{\pi(p)},d\pi_p(v)).
\end{align*}
Thus
\begin{align*}
(\pi^*(\iota_{Y_\mu}\omega_\mu))_p(v)=\omega_{\mu,\pi(p)}(d\pi_p((X_Z)_p),d\pi_p(v)).
\end{align*}
By the reduced-form identity,
\begin{align*}
\omega_{\mu,\pi(p)}(d\pi_p((X_Z)_p),d\pi_p(v))=(i^*\omega)_p((X_Z)_p,v).
\end{align*}
Since $di_p((X_Z)_p)=(X_H)_p$ and $di_p(v)=v$ under the inclusion $i:Z\to M$, this equals
\begin{align*}
\omega_p((X_H)_p,v)=dH_p(v).
\end{align*}
Since $H|_Z=\pi^*H_\mu$, we have
\begin{align*}
dH_p(v)=d(H|_Z)_p(v)=d(\pi^*H_\mu)_p(v).
\end{align*}
Therefore
\begin{align*}
\pi^*(\iota_{Y_\mu}\omega_\mu)=\pi^*dH_\mu.
\end{align*}
Because $\pi$ is a surjective submersion, pullback by $\pi$ is injective on differential forms: a form on $M_\mu$ is determined pointwise by its values on tangent vectors lifted through the surjective maps $d\pi_p:T_pZ\to T_{\pi(p)}M_\mu$. Hence
\begin{align*}
\iota_{Y_\mu}\omega_\mu=dH_\mu.
\end{align*}
By nondegeneracy of $\omega_\mu$, the vector field satisfying this equation is unique, so
\begin{align*}
Y_\mu=X_{H_\mu}.
\end{align*}
[guided]
We want to prove that the descended vector field is the Hamiltonian vector field of the descended Hamiltonian. The defining equation to prove on $M_\mu$ is
\begin{align*}
\iota_{Y_\mu}\omega_\mu=dH_\mu.
\end{align*}
Because $\pi:Z\to M_\mu$ is a surjective submersion, it is enough to pull back both one-forms by $\pi$; injectivity follows because every tangent vector in $T_{\pi(p)}M_\mu$ has a lift in $T_pZ$ through the surjective map $d\pi_p$.
Let $p\in Z$ and $v\in T_pZ$. Using the definition of interior product and the relation $d\pi_p((X_Z)_p)=(Y_\mu)_{\pi(p)}$, we get
\begin{align*}
(\pi^*(\iota_{Y_\mu}\omega_\mu))_p(v)=\omega_{\mu,\pi(p)}(d\pi_p((X_Z)_p),d\pi_p(v)).
\end{align*}
The reduced symplectic form is defined by $\pi^*\omega_\mu=i^*\omega$, so the last expression equals
\begin{align*}
(i^*\omega)_p((X_Z)_p,v).
\end{align*}
Since $i:Z\to M$ is the inclusion and $di_p((X_Z)_p)=(X_H)_p$, this is
\begin{align*}
\omega_p((X_H)_p,v)=dH_p(v),
\end{align*}
where the final equality is the Hamiltonian equation $\iota_{X_H}\omega=dH$ on $M$.
Finally, $H|_Z=\pi^*H_\mu$, so for $v\in T_pZ$,
\begin{align*}
dH_p(v)=d(H|_Z)_p(v)=d(\pi^*H_\mu)_p(v).
\end{align*}
Thus $\pi^*(\iota_{Y_\mu}\omega_\mu)=\pi^*dH_\mu$. Injectivity of pullback by the surjective submersion $\pi$ gives $\iota_{Y_\mu}\omega_\mu=dH_\mu$. Since $\omega_\mu$ is nondegenerate, the vector field satisfying this Hamiltonian equation is unique, and therefore $Y_\mu=X_{H_\mu}$.
[/guided]
[/step]
[step:Project integral curves to integral curves of the reduced Hamiltonian]
Let $I\subset\mathbb R$ be the time interval under consideration, and let
\begin{align*}
\gamma:I\to Z
\end{align*}
be an integral curve of $X_H$ with image in $Z$. Define
\begin{align*}
\gamma_\mu:I\to M_\mu,\qquad t\mapsto \pi(\gamma(t)).
\end{align*}
For every $t\in I$, the chain rule gives
\begin{align*}
\frac{d\gamma_\mu}{dt}(t)=d\pi_{\gamma(t)}\left(\frac{d\gamma}{dt}(t)\right).
\end{align*}
Since $\gamma$ is an integral curve of $X_H$ and $X_Z=X_H|_Z$, this becomes
\begin{align*}
\frac{d\gamma_\mu}{dt}(t)=d\pi_{\gamma(t)}((X_Z)_{\gamma(t)}).
\end{align*}
By the definition of $Y_\mu$,
\begin{align*}
d\pi_{\gamma(t)}((X_Z)_{\gamma(t)})=(Y_\mu)_{\gamma_\mu(t)}.
\end{align*}
Since $Y_\mu=X_{H_\mu}$, we conclude that
\begin{align*}
\frac{d\gamma_\mu}{dt}(t)=(X_{H_\mu})_{\gamma_\mu(t)}
\end{align*}
for every $t\in I$. Thus $\gamma_\mu$ is an integral curve of the reduced Hamiltonian vector field $X_{H_\mu}$. This proves the theorem.
[/step]
