Hilbert basis theorem
Statement
Theorem. If $R$ is a Noetherian ring, then $R[x]$ is a Noetherian ring.
Proof. Let $I\subset R[x]$ be an ideal. We want to show that $I$ is finitely generated. Let $f_1$ be a nonzero element of the minimal possible degree in $I$. For $i\geq 1$, if $(f_1,\dots,f_i)=I\neq I$, then choose $f_{i+1}$ to be an element of the minimal possible degree in $I\setminus (f_1,\dots,f_i)$. If $(f_1,\dots,f_i)=I$ then stop choosing elements- we have demonstrated that $I$ is finitely generated. So suppose this process doesn’t terminate in a finite number of steps.
For each $f_j$, let $a_j$ be the initial coefficient of $f_j$ (i.e. the coefficient of the highest degree term). Then the ideal generated by the $a_j$ is finitely generated since that ideal is in $R$ and $R$ is Noetherian. Since the collection of all $a_j$ generate this ideal, we can take a finite subcollection $(a_1,\dots,a_m)$ that will generate it. We claim that $I=(f_1,\dots,f_m)$.
Suppose otherwise. Consider $f_{m+1}$. Since the ideal generated by all $a_j$ is equal to the one generated by the $a_1,\dots,a_m$, we can write $a_{m+1}=\sum_{j=1}^m u_ja_j$ for some $u_j\in R$. Observe that $$ g=\sum_{j=1}^m u_jf_jx^{\deg f_{m+1}-\deg f_j}\in (f_1,\dots, f_m) $$ has the same degree and initial term as $f_{m+1}$ (indeed, each factor has degree equal to that of $f_{m+1}$ and $x$ to that power can be factored out of each summand leaving with a coefficient of $\sum_{j=1}^m u_ja_j=a_{m+1}$).
But this would imply $f_{m+1}-g\notin (f_1,\dots,f_m)$ since $f_{m+1}$ is not in that ideal. The difference is in $I$, however. But $g$ has degree strictly less than $f_{m+1}$ This contradicts the choice of $f_{m+1}$ being the one of minimal degree in $I\setminus (f_1,\dots,f_m)$. Thus it must be the case that $I=(f_1,\dots,f_m)$. $\square$