Let $\mathfrak{g}$ be a finite-dimensional Lie algebra over a field $k$, with an ordered basis $x_1 < x_2 < ... < x_n$.

We define the universal enveloping algebra $U(\mathfrak{g})$ of $\mathfrak{g}$ to be the free noncommutative algebra $k\langle x_1,...,x_n\rangle$ modulo the relations $(x_ix_j - x_jx_i = [x_i,x_j])$.

The Poincaré–Birkhoff–Witt (PBW) theorem states that $U(\mathfrak{g})$ has a basis consisting of lexicographically ordered monomials i.e. monomials of the form $x_1^{e_1}x_2^{e_2}...x_n^{e_n}$. Checking that this basis spans $U(\mathfrak{g})$ is trivial, so the work lies in showing that these monomials are linearly independent.

One standard proof of PBW is to construct a $\mathfrak{g}$-action on the commutative polynomial ring $k[y_1,...,y_n]$ by setting $x_1^{e_1}x_2^{e_2}...x_n^{e_n}\cdot 1 = y_1^{e_1}y_2^{e_2}...y_n^{e_n}$ and verify algebraically that this gives rise to a well-defined representation of $\mathfrak{g}$. Details can be found in Dixmier's book on enveloping algebras.

What other proofs of PBW are there out there?

Are there nice reformulations of the above proof from a different perspective, such as one that emphasizes the universal property of $U(\mathfrak{g})$?

However, I would be especially interested in learning about proofs which are not just repackaged versions of the same algebraic manipulations used in the above proof (for example, geometric proofs which appeal to some property of $U(\mathfrak{g})$ as differential operators, etc.). If we allow ourselves more tools than just plain algebra, what other proofs of PBW can we get?