[proofplan]
We use the PBW triangular factorisation to separate the negative, Cartan, and positive parts inside $U(\mathfrak g)$. Since the Verma module is induced from the one-dimensional $\mathfrak b$-module $\mathbb C_\lambda$, the $U(\mathfrak b)$-factor can be moved across the [tensor product](/page/Tensor%20Product) and evaluated on $1\in\mathbb C_\lambda$. This identifies $M(\lambda)$ with $U(\mathfrak n^-)\otimes\mathbb C_\lambda$, and under this identification $u\otimes 1$ is exactly $u v_\lambda$.
[/proofplan]
[step:Use PBW to split $U(\mathfrak g)$ into negative and Borel factors]
Let
\begin{align*}
m:U(\mathfrak n^-)\otimes U(\mathfrak h)\otimes U(\mathfrak n^+)&\longrightarrow U(\mathfrak g)
\end{align*}
\begin{align*}
u_-\otimes u_0\otimes u_+&\longmapsto u_-u_0u_+
\end{align*}
be the multiplication map. By [citetheorem:9359], $m$ is a [vector space](/page/Vector%20Space) isomorphism.
Since $\mathfrak b=\mathfrak h\oplus\mathfrak n^+$, the PBW theorem applied to the ordered basis with the $\mathfrak h$-basis before the $\mathfrak n^+$-basis identifies $U(\mathfrak b)$ with the subspace of $U(\mathfrak g)$ spanned by products $u_0u_+$ with $u_0\in U(\mathfrak h)$ and $u_+\in U(\mathfrak n^+)$. Hence multiplication gives a vector space isomorphism
\begin{align*}
\mu:U(\mathfrak n^-)\otimes U(\mathfrak b)&\longrightarrow U(\mathfrak g)
\end{align*}
\begin{align*}
u_-\otimes b&\longmapsto u_-b.
\end{align*}
Moreover, $\mu$ is a right $U(\mathfrak b)$-[module homomorphism](/page/Module%20Homomorphism), where $U(\mathfrak n^-)\otimes U(\mathfrak b)$ is given the right action
\begin{align*}
(u_-\otimes b)\cdot b'=u_-\otimes bb'
\end{align*}
for $u_-\in U(\mathfrak n^-)$ and $b,b'\in U(\mathfrak b)$.
[guided]
The point of PBW is that it gives a unique normal form for elements of $U(\mathfrak g)$. We choose an ordered basis compatible with the [direct sum](/page/Direct%20Sum) decomposition
\begin{align*}
\mathfrak g=\mathfrak n^-\oplus \mathfrak h\oplus \mathfrak n^+,
\end{align*}
putting basis vectors from $\mathfrak n^-$ first, then those from $\mathfrak h$, then those from $\mathfrak n^+$. The triangular PBW factorisation [citetheorem:9359] says that the multiplication map
\begin{align*}
m:U(\mathfrak n^-)\otimes U(\mathfrak h)\otimes U(\mathfrak n^+)&\longrightarrow U(\mathfrak g)
\end{align*}
\begin{align*}
u_-\otimes u_0\otimes u_+&\longmapsto u_-u_0u_+
\end{align*}
is a vector space isomorphism.
Now $\mathfrak b=\mathfrak h\oplus\mathfrak n^+$, so the same PBW ordering inside the [Lie algebra](/page/Lie%20Algebra) $\mathfrak b$ identifies $U(\mathfrak b)$ with the vector space spanned by products $u_0u_+$, where $u_0\in U(\mathfrak h)$ and $u_+\in U(\mathfrak n^+)$. Combining this with the triangular PBW factorisation, multiplication gives a vector space isomorphism
\begin{align*}
\mu:U(\mathfrak n^-)\otimes U(\mathfrak b)&\longrightarrow U(\mathfrak g)
\end{align*}
\begin{align*}
u_-\otimes b&\longmapsto u_-b.
\end{align*}
This is the exact structural input needed for induction. The Verma module tensors over $U(\mathfrak b)$, so we want the $U(\mathfrak b)$-part to sit as the right tensor factor. The map $\mu$ has precisely that compatibility: for $b'\in U(\mathfrak b)$,
\begin{align*}
\mu((u_-\otimes b)\cdot b')=\mu(u_-\otimes bb')=u_-bb'=\mu(u_-\otimes b)b'.
\end{align*}
Thus $\mu$ is not only a vector space isomorphism but also a right $U(\mathfrak b)$-module isomorphism.
[/guided]
[/step]
[step:Tensor the PBW splitting with the highest weight line]
Define
\begin{align*}
\Theta:U(\mathfrak n^-)\otimes \mathbb C_\lambda&\longrightarrow U(\mathfrak g)\otimes_{U(\mathfrak b)}\mathbb C_\lambda
\end{align*}
\begin{align*}
u_-\otimes c&\longmapsto u_-\otimes c.
\end{align*}
Here the tensor on the left is over $\mathbb C$, while the tensor on the right is over $U(\mathfrak b)$, and the displayed formula uses the inclusion $U(\mathfrak n^-)\subset U(\mathfrak g)$.
Using the right $U(\mathfrak b)$-module isomorphism $\mu$ from the previous step, we have vector space isomorphisms
\begin{align*}
U(\mathfrak g)\otimes_{U(\mathfrak b)}\mathbb C_\lambda
\cong (U(\mathfrak n^-)\otimes U(\mathfrak b))\otimes_{U(\mathfrak b)}\mathbb C_\lambda
\cong U(\mathfrak n^-)\otimes \mathbb C_\lambda.
\end{align*}
Under these isomorphisms, $\Theta$ is the inverse map. Therefore $\Theta$ is a vector space isomorphism.
Explicitly, the second isomorphism is induced by
\begin{align*}
(u_-\otimes b)\otimes c\longmapsto u_-\otimes bc,
\end{align*}
with inverse
\begin{align*}
u_-\otimes c\longmapsto (u_-\otimes 1)\otimes c.
\end{align*}
The balancing relation is respected because
\begin{align*}
((u_-\otimes b)b')\otimes c=(u_-\otimes bb')\otimes c
\end{align*}
and
\begin{align*}
(u_-\otimes b)\otimes b'c
\end{align*}
both map to $u_-\otimes bb'c$.
[/step]
[step:Identify the induced generator with the highest weight vector]
By definition,
\begin{align*}
v_\lambda=1\otimes 1\in U(\mathfrak g)\otimes_{U(\mathfrak b)}\mathbb C_\lambda=M(\lambda).
\end{align*}
For $u\in U(\mathfrak n^-)$, the left $U(\mathfrak g)$-module structure on $M(\lambda)$ gives
\begin{align*}
u v_\lambda=u(1\otimes 1)=u\otimes 1.
\end{align*}
Thus the map
\begin{align*}
\Psi_\lambda:U(\mathfrak n^-)&\longrightarrow M(\lambda)
\end{align*}
\begin{align*}
u&\longmapsto u v_\lambda
\end{align*}
is the composite of the vector space isomorphism
\begin{align*}
U(\mathfrak n^-)&\longrightarrow U(\mathfrak n^-)\otimes\mathbb C_\lambda
\end{align*}
\begin{align*}
u&\longmapsto u\otimes 1
\end{align*}
with the vector space isomorphism $\Theta$. Hence $\Psi_\lambda$ is a vector space isomorphism.
[/step]
[step:Interpret the isomorphism as freeness over $U(\mathfrak n^-)$]
The map $\Psi_\lambda$ is compatible with left multiplication by $U(\mathfrak n^-)$. Indeed, for $a,u\in U(\mathfrak n^-)$,
\begin{align*}
\Psi_\lambda(au)=(au)v_\lambda=a(uv_\lambda)=a\Psi_\lambda(u).
\end{align*}
Thus $M(\lambda)$ is a free left $U(\mathfrak n^-)$-module of rank $1$ with generator $v_\lambda$.
The defining relations from the inducing module are
\begin{align*}
xv_\lambda=0\quad\text{for every }x\in\mathfrak n^+
\end{align*}
and
\begin{align*}
hv_\lambda=\lambda(h)v_\lambda\quad\text{for every }h\in\mathfrak h.
\end{align*}
The freeness just proved means that these relations impose no nonzero relation of the form $u v_\lambda=0$ with $u\in U(\mathfrak n^-)$. This is precisely the asserted PBW model of the Verma module.
[/step]
