[proofplan]
The equations $\partial_{\alpha_j}S=\beta_j$ define $y$ locally by the inverse function theorem because the mixed matrix $S_{y\alpha}$ is invertible. Differentiating these equations with respect to $x$ gives a linear system involving $y'$. Differentiating the Hamilton-Jacobi equation with respect to $\alpha$ gives the same linear system with $\partial_pH$ in place of $y'$, so invertibility forces $y'=\partial_pH$. Differentiating $p=\nabla_yS$ and using the $y$-derivative of the Hamilton-Jacobi equation gives $p'=-\partial_yH$.
[/proofplan]
[step:Use the nondegeneracy condition to solve for $y$ locally]
Define $F:I\times V\to\mathbb{R}^n$ by
\begin{align*}
F(x,y):=\nabla_\alpha S(x,y,\alpha_0)-\beta.
\end{align*}
The hypotheses give $F(x_0,y_0)=0$. The derivative of $F$ with respect to $y$ at $(x_0,y_0)$ is the [linear map](/page/Linear%20Map) represented by $M_0^\top$, because the $j$th component of $F$ is $\partial_{\alpha_j}S-\beta_j$. Since $M_0$ is invertible, $M_0^\top$ is invertible. By the [Inverse Function Theorem](/theorems/51), after shrinking to a neighbourhood of $x_0$, there is an open interval $J\subset I$ containing $x_0$ and a $C^1$ curve $y:J\to V$ with $y(x_0)=y_0$ such that
\begin{align*}
F(x,y(x))=0
\end{align*}
for every $x\in J$. Equivalently,
\begin{align*}
\partial_{\alpha_j}S(x,y(x),\alpha_0)=\beta_j
\end{align*}
for every $j=1,\ldots,n$.
[guided]
The system $\nabla_\alpha S(x,y,\alpha_0)=\beta$ is meant to determine the unknown $y$ as a function of $x$. To use the inverse function theorem, we freeze the parameter $\alpha_0$ and define
\begin{align*}
F(x,y)=\nabla_\alpha S(x,y,\alpha_0)-\beta.
\end{align*}
At the base point, the equations in the statement say $F(x_0,y_0)=0$.
The derivative of $F$ with respect to $y$ has entries
\begin{align*}
\partial_{y_i}F_j(x_0,y_0)=\partial_{y_i}\partial_{\alpha_j}S(x_0,y_0,\alpha_0).
\end{align*}
Thus $D_yF(x_0,y_0)$ is represented by $M_0^\top$. Since $M_0$ is invertible, this derivative is an isomorphism. The [Inverse Function Theorem](/theorems/51) therefore solves $F(x,y)=0$ uniquely for $y$ as a $C^1$ function of $x$ near $x_0$. This gives a curve $y:J\to V$ satisfying
\begin{align*}
\nabla_\alpha S(x,y(x),\alpha_0)=\beta
\end{align*}
for all $x\in J$.
[/guided]
[/step]
[step:Differentiate the parameter equations to obtain the first Hamilton equation]
For $x\in J$, set
\begin{align*}
p(x):=\nabla_yS(x,y(x),\alpha_0).
\end{align*}
Differentiate the identity
\begin{align*}
\nabla_\alpha S(x,y(x),\alpha_0)=\beta
\end{align*}
with respect to $x$. Since $\beta$ is constant, this gives
\begin{align*}
S_{x\alpha}(x,y(x),\alpha_0)+S_{y\alpha}(x,y(x),\alpha_0)^\top y'(x)=0.
\end{align*}
Now differentiate the Hamilton-Jacobi equation
\begin{align*}
\partial_xS(x,y,\alpha_0)+H(x,y,\nabla_yS(x,y,\alpha_0))=0
\end{align*}
with respect to $\alpha$ while holding $(x,y)$ fixed. The chain rule gives
\begin{align*}
S_{x\alpha}(x,y,\alpha_0)+S_{y\alpha}(x,y,\alpha_0)^\top\partial_pH(x,y,\nabla_yS(x,y,\alpha_0))=0.
\end{align*}
Evaluating at $y=y(x)$ and using $p(x)=\nabla_yS(x,y(x),\alpha_0)$, we obtain
\begin{align*}
S_{y\alpha}(x,y(x),\alpha_0)^\top\left(y'(x)-\partial_pH(x,y(x),p(x))\right)=0.
\end{align*}
After shrinking $J$ if necessary, $S_{y\alpha}(x,y(x),\alpha_0)$ remains invertible by continuity and the invertibility of $M_0$. Hence
\begin{align*}
y'(x)=\partial_pH(x,y(x),p(x)).
\end{align*}
[/step]
[step:Differentiate the momentum definition to obtain the second Hamilton equation]
Differentiate
\begin{align*}
p(x)=\nabla_yS(x,y(x),\alpha_0)
\end{align*}
with respect to $x$. This gives
\begin{align*}
p'(x)=S_{xy}(x,y(x),\alpha_0)+S_{yy}(x,y(x),\alpha_0)y'(x).
\end{align*}
Differentiate the Hamilton-Jacobi equation with respect to $y$ while holding $\alpha_0$ fixed:
\begin{align*}
S_{xy}(x,y,\alpha_0)+S_{yy}(x,y,\alpha_0)\partial_pH(x,y,\nabla_yS(x,y,\alpha_0))+\partial_yH(x,y,\nabla_yS(x,y,\alpha_0))=0.
\end{align*}
Evaluate this identity at $y=y(x)$ and use the first Hamilton equation $y'(x)=\partial_pH(x,y(x),p(x))$. The previous two displays combine to give
\begin{align*}
p'(x)=-\partial_yH(x,y(x),p(x)).
\end{align*}
Together with the first Hamilton equation, this proves that $(y,p)$ solves Hamilton's equations on $J$.
[/step]
