Ado's theorem and the reduction to positive characteristic

Question

The synopsis: proofs of Ado theorem in positive characteristic are simple, and in characteristic $0$ are difficult. Can one infer the characteristic $0$ case from the positive characteristic case?

The context

Ado's theorem ensures that any finite-dimensional Lie algebra has a faithful representation:

Let $K$ be an arbitrary field and $\frak g$ a finite dimensional Lie algebra over $K$. Then there exists an injective homomorphism of Lie algebras ${\frak g}\to {\frak gl}(n,K)$ for some natural number $n$.

Its proof for $K$ of characteristic $0$ is, perhaps unexpectedly, quite involved and requires the prior development of much of the structural theory.

On the other hand, the characteristic $p$ case is quite simple modulo the Poincaré-Birkhoff-Witt theorem: the naive idea of using the PBW embedding to the universal enveloping algebra actually works out after taking a suitable quotient. Here is a sketch of the argument (due to Jacobson):

1. In $U(\frak g)$ one has $ad_x^my=\sum_{i=0}^m (-1)^i \binom{m}{i} x^iyx^{m-i}$ and if $m=p$ then each $\binom{p}{i}=0$ unless $i=0,p$. Thus $ad_x^p y=ad_{x^p} y$ and hence $ad_x^{p ^i}y=ad_{x^{p ^i}} y$ for any $i$.

2. Let $Q(X)$ be a minimal polynomial of $ad_x$, so $Q(ad_x)=0$. By euclidean division $X^{p^i}=Q(X)U_i(X)+R_i(X)$, where $\deg R_i<\deg Q\le \dim \frak g$. Since the space of polynomials of degree $<\dim \frak g$ has dimension $\dim \frak g$ there is a nontrivial linear combination $\sum_{i=0}^{\dim \frak g} \lambda_iR_i(X)=0$ and hence $Q(X)\sum_{i=0}^{\dim \frak g}\lambda_iU_i(X)=\sum_{i=0}^{\dim \frak g}\lambda_iX^{p^i}$. In particular, $ad_x$ is annihilated by $\sum_{i=0}^{\dim \frak g}\lambda_iX^{p^i}$.

3. By combining Step 1 and Step 2 one obtains $\sum_{i=0}^{\dim \frak g}\lambda_i ad_x^{p^i}=\sum_{i=0}^{\dim \frak g}\lambda_i ad_{x^{p^i}}=ad_{\sum_{i=0}^{\dim \frak g} \lambda_ix^{p^i}}=0$. In other words, $\sum_{i=0}^{\dim \frak g}\lambda_ix^{p^i}$ is central in $U(\frak g)$. Thus for any $x_i$ from some basis of $\frak g$ one has a decomposition $x_i^{p^{n_i}}=z_i+P_i(x_i)$ where $z_i$ is central and $\deg P_i<p^{n_i}$, where $n_i\le \dim \frak g$.

4. Let $I\subset U(\frak g)$ be an ideal generated by all $z_i$ from the previous step. By PBW $x_1^{k_1}\dots x_{\dim \frak g}^{k_{\dim \frak g}}$ is a basis of $U(\frak g)$. The elements of the form $\bar x_1^{\alpha_1}\dots \bar x_{\dim \frak g}^{\alpha_{\dim \frak g}}$ where $\alpha_i<p^{n_i}$ make up a basis of $U({\frak g})/I$. Indeed, they span everything because if some $\alpha_i\ge p^{n_i}$, then using the decomposition $x_i^{p^{n_i}}=z_i+P_i(x_i)$ we can rewrite the monomial as a sum of monomials in which $\bar x_i$ occurs with degree $<\alpha_i$. Linear independence obviously follows from the linear independence of $x_1^{k_1}\dots x_{\dim \frak g}^{k_{\dim \frak g}}$ in $U(\frak g)$. So $U({\frak g})/I$ is an associative algebra of dimension $\le (p^{\dim(\frak g)})^{\dim \frak g}$.

5. Then, as usual, embed $U({\frak g})/I$ to ${\frak{gl}}(U({\frak g})/I)$ using its action on itself by right multiplication. Note that the dimension of representation thus obtained is $\le p^{2\cdot\dim^2(\frak g)}$.

Another, more compact, way to phrase this is to introduce the notion of a restricted Lie algebra, show that there is the corresponding version of PBW for restricted universal enveloping algebras, which are always finite-dimensional, and to notice that any Lie algebra admits an embedding into a f.d. restricted Lie algebra.

The question

Is there a proof of Ado theorem (assuming algebraic closedness, if inevitable) by reduction to the positive characteristic case?

The first thing that comes to mind is to use the fact that the ultraproduct of all prime algebraically closed fields is elementary equivalent to the field of complex numbers: $\text{ulim}_{p\to\infty}\bar{\mathbb{F}}_p\cong\mathbb C$. The statement about a field “Each $m$-dimensional Lie algebra over me has a faithful representation of dimension $n$” is a first order sentence in the language of fields (actually an algebraic condition), but unfortunately the dimensions of faithful representations given by Jacobson's characteristic $p$ proof grow indefinitely with $p$. On the other hand the sentence “Each $m$-dimensional Lie algebra over me has a finite-dimensional faithful representation” does not seem like a first-order sentence in $ACF_0$.

I hope that there might be some smarter choice of the language, theory and coding, which could rescue this (“model theoretic”) approach.

I am aware of the existence of other “reduction to char. $p$” methods in mathematics (starting with the Hensel lemma!) so would love to know if any of them apply here.