I decided to prove that for any field $k$,
dim $k[x_1, \ldots, x_n] = n$.
Every proof I've seen follows either of these two approaches:
Noether normalisation (first prove that if $A$ is a finitely generated domain over $k$, then $\dim A = \text{trdeg}(K(A)/k)$. Now the desired result is a special case.)
Going down theorem.
However I believe I've written a proof which is independent of either of these results (and is more elementary). Can someone please verify this?
Lemma. If $A \to B$ is an integral extension of rings, then $\dim A = \dim B$. This follows from the going up theorem.
Proof that $\dim k[x_1, \ldots, x_n] = n$. It's clear that $\dim k[x_1, \ldots, x_n] \geq n$, so we proceed by induction on $n$ to show that $\dim k[x_1, \ldots, x_n] \leq n$. The base case is trivial. Now fix $m$, and suppose $\dim k[x_1, \ldots, x_m] = m$. Suppose for a contradiction that $\dim k[x_1, \ldots, x_{m+1}] > m+1$, and let $P_0 \subset \cdots \subset P_{s}$ be a strictly increasing chain of prime ideals in $k[x_1, \ldots, x_{m+1}]$ with $s > m+1$. Assume without loss of generality that $P_0 = 0$. Choose any non-zero element of $P_1$, and decompose it into irreducible factors. Since $P_1$ is prime, at least one of these factors $f$ lies in $P_1$, so now consider the strictly increasing chain of primes $$0 \subset (f) \subset \cdots \subset P_s.$$ Since $f$ has degree at least 1, choose any $x_i$ that appears in the expression of $f(x_1, \ldots, x_{m+1})$. (Without loss of generality, $x_i = x_{m+1}$.) Viewing $f$ as a polynomial in $k[x_1, \ldots, x_{m}][x_{m+1}]$, it is still irreducible, so we now have a finite (hence integral) extension $$k[x_1, \ldots, x_m] \to \frac{k[x_1, \ldots, x_m][x_{m+1}]}{(f)}.$$ By the earlier lemma and the inductive hypothesis, the right side has dimension $m$. But this is a contradiction, since the chain of primes $(f) \subset \cdots \subset P_s$ descends to a strictly increasing chain of prime ideals in $\frac{k[x_1, \ldots, x_m][x_{m+1}]}{(f)}$, of length $s-1 > m$. Therefore $\dim k[x_1, \ldots, x_n] \leq n$ for any $n$, as required.
I feel like the only ``non-elementary" step was the use of the going up theorem, but this is quite distinct from NNL or going down (and somehow feels more elementary than those) so I'd appreciate if someone could verify this. Thank you!
The extension $k[x_1,\ldots,x_m] \to \frac{k[x_1,\ldots,x_m][x_{m+1}]}{(f)}$ is not necessarily integral. For example, the ring of Laurent polynomials $k[x,y]/(xy-1)\cong k[x,x^{-1}]$ is not integral over $k[x]$.
However, it can be made integral by performing a change of coordinates (and doing so fixes this proof).
Lemma 13.2 of Eisenbud's Commutative Algebra with a View Towards Algebraic Geometry applied to this situation tells us that there are elements $x_1',\ldots,x_m'\in k[x_1,\ldots,x_{m+1}]$ such that $k[x_1,\ldots,x_{m+1}]/(f)$ is finite over $k[x_1',\ldots,x_m']$. The lemma further states that if $d$ is a sufficiently large positive integer, then we may let $x_i'=x_i-x_{m+1}^{d^i}$ (in fact, if $k$ is an infinite field then $x_i=x_i-a_ix_{m+1}$ works for some $a_i\in k$). In particular, the $x_i'$ can be chosen to be algebraically independent, so that $k[x_1',\ldots,x_m']\cong k[x_1,\ldots,x_m]$, and so the induction step in your proof works.
Lemma 13.2 is crucially applied in the proof of Noether Normalization (Theorem 13.3), so I think it is fair to say this proof approach is really not too different from applying Noether Normalization directly.