[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*}[/step]

[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: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*}[/step]

[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: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]