The derived algebra of a solvable Lie algebra is nilpotent in characteristic zero

Choose one finite basis $e_1,\dots ,e_n$ of $\mathfrak{g}$ and let $k_0\subseteq k$ be the subfield generated over $\mathbb{Q}$ by the finitely many structure constants in $[e_i,e_j]={\sum }_s{c}_{ij}^s{e}_s$. The same table defines a $k_0$-Lie algebra ${\mathfrak{g}}_0$ with $k{\otimes }_{k_0}{\mathfrak{g}}_0\cong \mathfrak{g}$ as in [L5]. Direct expansion of pure tensors and induction give $(K{\otimes }_F\mathfrak{a}{)}^{(r)}=K{\otimes }_F{\mathfrak{a}}^{(r)}$ and ${\gamma }_r(K{\otimes }_F\mathfrak{a})=K{\otimes }_F{\gamma }_r(\mathfrak{a})$ for every field extension $K\mathrm{/}F$. Scalar extension is faithful on a finite-dimensional vector space because a basis remains a basis. Hence solvability of $\mathfrak{g}$ implies solvability of ${\mathfrak{g}}_0$.

The finitely generated field $k_0\mathrm{/}\mathbb{Q}$ is countable with an explicit enumeration by rational expressions. In ZF, build an algebraic closure $K$ by a deterministic countable tower: dovetail all polynomials over earlier stages, choose the first coded monic irreducible factor, adjoin one root, and take the union. Every polynomial over the union occurs at a finite stage and later gains a root, so the union is algebraically closed. Put $\mathfrak{G}=K{\otimes }_{k_0}{\mathfrak{g}}_0$; step 1.1 makes $\mathfrak{G}$ finite-dimensional and solvable. No choice function is used in this fixed enumeration.

The homomorphic image $\mathrm{ad}(\mathfrak{G})$ is solvable because its derived terms are images of those of $\mathfrak{G}$. It is a linear Lie algebra on $\mathfrak{G}$, so [L1] says its derived algebra $[\mathrm{ad}(\mathfrak{G}),\mathrm{ad}(\mathfrak{G})]=\mathrm{ad}({\mathfrak{G}}^{\mathrm{\prime }})$ is nilpotent.

Restrict $\mathrm{ad}$ to ${\mathfrak{G}}^{\mathrm{\prime }}$. By [L3] its kernel is ${\mathfrak{G}}^{\mathrm{\prime }}\cap Z(\mathfrak{G})$, which is central in ${\mathfrak{G}}^{\mathrm{\prime }}$, and by [L4] the quotient by this kernel is isomorphic to the nilpotent image $\mathrm{ad}({\mathfrak{G}}^{\mathrm{\prime }})$ from step 3.1. The central-extension result [L2] therefore makes ${\mathfrak{G}}^{\mathrm{\prime }}$ nilpotent.

If ${\gamma }_{c+1}({\mathfrak{G}}^{\mathrm{\prime }})=0$, the scalar-extension identities of step 1.1 give $0=K{\otimes }_{k_0}{\gamma }_{c+1}({\mathfrak{g}}_0^{\mathrm{\prime }})$, so faithfulness gives ${\gamma }_{c+1}({\mathfrak{g}}_0^{\mathrm{\prime }})=0$. Extending from $k_0$ to $k$ then gives ${\mathfrak{g}}^{\mathrm{\prime }}=k{\otimes }_{k_0}{\mathfrak{g}}_0^{\mathrm{\prime }}$ and ${\gamma }_{c+1}({\mathfrak{g}}^{\mathrm{\prime }})=0$. Thus ${\mathfrak{g}}^{\mathrm{\prime }}$ is nilpotent. Characteristic zero enters through $\mathbb{Q}\subseteq k$ and [L1]; the algebraic closure used in step 2.1 was constructed without AC.