Engel's common-zero-vector lemma

If $\mathfrak{g}=0$, every nonzero $v\in V$ is annihilated by $\mathfrak{g}$, so the assertion holds.

Assume $\mathfrak{g}\mathrm{\ne }0$ and that the assertion holds for every nil Lie algebra of operators of dimension strictly smaller than $\dim \mathfrak{g}$, acting on any nonzero finite-dimensional module.

Choose a proper subalgebra $\mathfrak{h}<\mathfrak{g}$ of maximal dimension; this exists because $0$ is proper and the possible dimensions form a nonempty finite set. For $H\in \mathfrak{h}$, take $m>0$ with $H^m=0$ by [L1]. On $\mathrm{End}(V)$, ${\mathrm{ad}}_H=L_H-R_H$, where $L_H$ and $R_H$ commute, and every term of $(L_H-R_H{)}^{2m-1}$ contains either $L_H^m$ or $R_H^m$; hence ${\mathrm{ad}}_H$ is nilpotent. Its restrictions and induced quotient operators are nilpotent as well.

The adjoint action of $\mathfrak{h}$ preserves $\mathfrak{h}$, so [L2] gives an action on the nonzero space $\mathfrak{g}\mathrm{/}\mathfrak{h}$. By step 1.3 it is nil, and step 1.2 supplies a nonzero coset $x+\mathfrak{h}$ killed by $\mathfrak{h}$. Thus $x\mathrm{\notin }\mathfrak{h}$ and $[\mathfrak{h},x]\subseteq \mathfrak{h}$, so the normalizer of $\mathfrak{h}$ strictly contains $\mathfrak{h}$.

The normalizer is a subalgebra; maximality of $\mathfrak{h}$ in step 1.3 and step 2.1 therefore make it all of $\mathfrak{g}$, so $\mathfrak{h}$ is an ideal. Moreover $\mathfrak{g}\mathrm{/}\mathfrak{h}$ is one-dimensional: otherwise the inverse image of the one-dimensional subalgebra spanned by any nonzero quotient vector would be strictly between $\mathfrak{h}$ and $\mathfrak{g}$. Hence $\mathfrak{g}=\mathfrak{h}\oplus kx$.

Apply step 1.2 to $\mathfrak{h}$ acting on $V$. Its common kernel $V_0=\{v\in V:\mathfrak{h}v=0\}$ is nonzero. It is $x$-stable, because for $H\in \mathfrak{h}$ and $v\in V_0$, $H(xv)=x(Hv)+[H,x]v=0$ by ideality from step 3.1.

The restriction of $x$ to nonzero finite-dimensional $V_0$ is nilpotent by [L1]. Its kernel is nonzero: if it were zero, rank-nullity [L3] would make $x{\mathrm{\mid }}_{V_0}$ injective, hence every positive power injective, contradicting nilpotence on $V_0\mathrm{\ne }0$. Choose $0\mathrm{\ne }v\in \ker (x{\mathrm{\mid }}_{V_0})$. Then $\mathfrak{h}v=0$, $xv=0$, and step 3.1 gives $\mathfrak{g}v=0$. This is a single finite existential choice, not an application of Choice.