Verma embedding for an arbitrary positive root

Put $n=⟨\lambda +\rho ,{\alpha }^{\vee }⟩>0$ and $\mu =\lambda -n\alpha =s_{\alpha }\cdot \lambda$. At weight $\lambda -n\alpha$, the determinant formula has the factor $⟨\lambda +\rho ,{\alpha }^{\vee }⟩-n$ with exponent $K(0)=1$. Thus its hyperplane is a factor hyperplane, and at generic points $\eta$ on it the generic-radical lemma supplies a nonzero singular vector in $M(\eta {)}_{\eta -n\alpha }$.

In fixed PBW coordinates the maps $e_i:M(\eta {)}_{\eta -n\alpha }\to M(\eta {)}_{\eta -n\alpha +{\alpha }_i}$ have matrix entries polynomial in $\eta$. Stack them to form one matrix $E(\eta )$. Step 1.1 says it has a nonzero kernel at a dense set of points on the affine hyperplane $H_{\alpha ,n}$. Hence every maximal minor of $E$ vanishes identically on that hyperplane: a polynomial that vanishes outside a countable union of proper affine subspaces there is zero. In particular $E(\lambda )$ has a nonzero kernel. A vector in it is killed by every simple positive-root vector, hence by all of ${\mathfrak{n}}^{+}$, and has weight $\mu$.

By [F1] this vector defines a nonzero map $M(\mu )\to M(\lambda )$, which is injective. Since $\mu =s_{\alpha }\cdot \lambda$, this is the required embedding.