[proofplan]
We prove the result by induction on $\beta \leq \alpha$. The base stage and limit stages follow directly from the recursive definition of the constructible hierarchy, once we know that $M$ and the ambient universe index the same earlier ordinals. The only substantive point is the successor step: if $L_\beta^M=L_\beta$, then transitivity makes the structure $(L_\beta,\in)$ and all of its parameters the same inside $M$ and externally, while the assumed satisfaction-coding fragment gives the same first-order truth relation for this set-sized structure. Therefore $M$ and the ambient universe form the same definable subsets of $L_\beta$.
[/proofplan]
[step:Run induction over the constructible stages up to $\alpha$]
We prove, by transfinite induction on ordinals $\beta \leq \alpha$, that
\begin{align*}
L_\beta^M = L_\beta.
\end{align*}
The induction is legitimate in the ambient universe. Moreover, if $\gamma < \beta \leq \alpha$, then $\gamma < \alpha$ unless $\beta=0$, so by hypothesis $\gamma \in M$. Thus the internal recursion in $M$ and the ambient recursion range over the same earlier ordinal indices below each nonzero stage $\beta \leq \alpha$.
[/step]
[step:Verify the initial level]
By definition of the constructible hierarchy, the ambient initial level is
\begin{align*}
L_0 = \varnothing.
\end{align*}
The same defining recursion is used inside $M$, so
\begin{align*}
L_0^M = \varnothing.
\end{align*}
Therefore $L_0^M=L_0$.
[/step]
[step:Identify limit levels by taking the same union of earlier stages]
Let $\lambda \leq \alpha$ be a limit ordinal, and assume that
\begin{align*}
L_\gamma^M = L_\gamma
\end{align*}
for every ordinal $\gamma < \lambda$. By the recursive definition of the constructible hierarchy in $M$,
\begin{align*}
L_\lambda^M = \bigcup_{\gamma < \lambda} L_\gamma^M.
\end{align*}
By the ambient recursive definition,
\begin{align*}
L_\lambda = \bigcup_{\gamma < \lambda} L_\gamma.
\end{align*}
The index class $\{\gamma : \gamma < \lambda\}$ is the same for both constructions because $M$ is transitive and contains all ordinals below $\alpha$. Substituting the induction hypothesis into the internal union gives
\begin{align*}
L_\lambda^M = \bigcup_{\gamma < \lambda} L_\gamma = L_\lambda.
\end{align*}
[guided]
Let $\lambda \leq \alpha$ be a limit ordinal. The constructible hierarchy has no new definability operation at a limit stage; it simply collects everything constructed earlier. Internally, $M$ computes
\begin{align*}
L_\lambda^M = \bigcup_{\gamma < \lambda} L_\gamma^M.
\end{align*}
Externally, the ambient universe computes
\begin{align*}
L_\lambda = \bigcup_{\gamma < \lambda} L_\gamma.
\end{align*}
We must check that these are unions over the same ordinals. Since $\lambda \leq \alpha$, every $\gamma < \lambda$ satisfies $\gamma < \alpha$ unless $\lambda=0$, and $\lambda$ is a limit ordinal here. The hypothesis says every ordinal below $\alpha$ belongs to $M$. Since $M$ is transitive, ordinal membership and the relation $\gamma < \lambda$ are interpreted the same way in $M$ and externally. Thus both unions are indexed by exactly the same earlier stages.
For each such $\gamma$, the induction hypothesis gives
\begin{align*}
L_\gamma^M = L_\gamma.
\end{align*}
Replacing every internal earlier level by the corresponding ambient earlier level yields
\begin{align*}
L_\lambda^M = \bigcup_{\gamma < \lambda} L_\gamma = L_\lambda.
\end{align*}
So the limit stage agrees.
[/guided]
[/step]
[step:Show that successor levels have the same definable subsets]
Let $\beta+1 \leq \alpha$, and assume that
\begin{align*}
L_\beta^M = L_\beta.
\end{align*}
By definition,
\begin{align*}
L_{\beta+1}^M = \operatorname{Def}^M(L_\beta^M,\in)
\end{align*}
and
\begin{align*}
L_{\beta+1} = \operatorname{Def}(L_\beta,\in).
\end{align*}
Using the induction hypothesis, it remains to prove
\begin{align*}
\operatorname{Def}^M(L_\beta,\in)=\operatorname{Def}(L_\beta,\in).
\end{align*}
Let $A \subseteq L_\beta$. By definition, $A \in \operatorname{Def}(L_\beta,\in)$ exactly when there are a first-order formula $\varphi(v,w_1,\dots,w_n)$ in the language $\{\in\}$ and parameters $a_1,\dots,a_n \in L_\beta$ such that
\begin{align*}
A=\{x \in L_\beta : (L_\beta,\in)\models \varphi(x,a_1,\dots,a_n)\}.
\end{align*}
The formula code is a natural number, hence belongs to $M$ because $M$ is transitive and satisfies the relevant Infinity fragment. Also $a_1,\dots,a_n \in L_\beta=L_\beta^M$, so the parameters belong to $M$. Since $(L_\beta,\in)$ is a set-sized structure in $M$ and $M$ has the assumed satisfaction-coding fragment, satisfaction for this structure is absolute between $M$ and the ambient universe:
\begin{align*}
M \models ``(L_\beta,\in)\models \varphi(x,a_1,\dots,a_n)''
\end{align*}
if and only if
\begin{align*}
(L_\beta,\in)\models \varphi(x,a_1,\dots,a_n)
\end{align*}
for every $x \in L_\beta$.
Therefore the same formula with the same parameters defines the same subset of $L_\beta$ inside $M$ and externally. Separation in $M$ forms this subset internally, and the ambient definition forms it externally. Hence
\begin{align*}
\operatorname{Def}^M(L_\beta,\in)=\operatorname{Def}(L_\beta,\in).
\end{align*}
Consequently,
\begin{align*}
L_{\beta+1}^M=L_{\beta+1}.
\end{align*}
[guided]
Let $\beta+1 \leq \alpha$, and suppose the previous levels agree:
\begin{align*}
L_\beta^M=L_\beta.
\end{align*}
At a successor stage, the constructible hierarchy does not take a union; it forms the subsets of the previous level that are first-order definable over that previous level. Thus $M$ computes
\begin{align*}
L_{\beta+1}^M=\operatorname{Def}^M(L_\beta^M,\in),
\end{align*}
while the ambient universe computes
\begin{align*}
L_{\beta+1}=\operatorname{Def}(L_\beta,\in).
\end{align*}
By the induction hypothesis, the underlying set of the structure is the same in both computations. So the problem reduces to showing that $M$ and the ambient universe agree about which subsets of $L_\beta$ are definable over $(L_\beta,\in)$.
Fix a subset $A \subseteq L_\beta$. Externally, $A$ is in $\operatorname{Def}(L_\beta,\in)$ exactly when there are a first-order formula $\varphi(v,w_1,\dots,w_n)$ in the language $\{\in\}$ and parameters $a_1,\dots,a_n \in L_\beta$ such that
\begin{align*}
A=\{x \in L_\beta : (L_\beta,\in)\models \varphi(x,a_1,\dots,a_n)\}.
\end{align*}
We now check that all data in this definition are also available inside $M$. The formula $\varphi$ is represented by a natural-number code, and the relevant fragment of ZF in $M$ includes the coding of syntax; since $M$ is transitive and satisfies the needed Infinity fragment, these finite syntactic codes are the same in $M$ as externally. The parameters $a_1,\dots,a_n$ lie in $L_\beta$, and $L_\beta=L_\beta^M$ by the induction hypothesis, so they are parameters available to $M$. Finally, the structure $(L_\beta,\in)$ is the same structure in both contexts: transitivity of $M$ makes membership between elements of $L_\beta$ absolute.
The remaining issue is truth in this set-sized structure. By the assumed satisfaction-coding fragment, $M$ has the satisfaction relation for $(L_\beta,\in)$, and this coded satisfaction relation agrees with the ambient one. Therefore, for every $x \in L_\beta$,
\begin{align*}
M \models ``(L_\beta,\in)\models \varphi(x,a_1,\dots,a_n)''
\end{align*}
if and only if
\begin{align*}
(L_\beta,\in)\models \varphi(x,a_1,\dots,a_n).
\end{align*}
Thus the same formula and the same parameters select exactly the same elements $x \in L_\beta$ inside $M$ and externally. Since $M$ has the required Separation fragment for formulas defining subsets of earlier levels, $M$ forms precisely that subset at the successor stage. This proves
\begin{align*}
\operatorname{Def}^M(L_\beta,\in)=\operatorname{Def}(L_\beta,\in),
\end{align*}
and hence
\begin{align*}
L_{\beta+1}^M=L_{\beta+1}.
\end{align*}
[/guided]
[/step]
[step:Conclude agreement through stage $\alpha$]
The base case, limit case, and successor case establish the induction for every ordinal $\beta \leq \alpha$. Therefore
\begin{align*}
L_\beta^M=L_\beta
\end{align*}
for all $\beta \leq \alpha$. This is exactly the assertion that the constructible hierarchy computed internally by $M$ agrees with the ambient constructible hierarchy through stage $\alpha$.
[/step]
