December 9th
Today I learned a generalization of Hensel's lemma. Fix $K$ complete with respect to a nonarchimedean valuation $|\cdot|$ so that we have\[\mathcal O_K:=\{\alpha\in K:|\alpha|\le1\}.\]This is our ring of integers in the local field, and $\mf p:=\{\alpha\in K:|\alpha| \lt 1\}$ is our unique maximal ideal.
Now, let $f(x)\in\mathcal O_K[x]$ be a polynomial such that $\overline f(x)\in(\mathcal O_K/\mf p)[x]$ is nonzero; i.e., "primitive.'' (Namely, scale the polynomial so that the biggest coefficient has absolute value $1.$) If $\overline f(x)=\overline g(x)\overline h(x)$ for polynomials $\overline g(x),\overline h(x)\in\mathcal(O_K/\mf p)[x]$ which are coprime. Then we claim can actually factor\[f(x)=g(x)h(x)\]for which $g\equiv\overline g$ and $h\equiv\overline h\pmod{\mf p}.$ Further, $\deg g=\deg\overline g.$
We do this using the same induction featured in Hensel's lemma. In other words, we're going to lift our polynomials upwards. So start with ant $g_0,h_0\in\mathcal O_K[x]$ with $\overline{g_0}=\overline g$ and $\overline{h_0}=\overline h$ with $\deg g_0=\deg g.$ But further, $\overline g$ and $\overline h$ being coprime lets us take $a,b\in\mathcal O_K[x]$ such that $\overline a\overline g+\overline b\overline h=1.$
Now surely $f-g_0h_0\in\mf p,$ and we can check the coefficient with the largest absolute value here to extract some $\pi\in\mf p$ such that\[f-g_0h_0\in(\pi).\]This follows from being a local ring—the ideals generated by each coefficient of this difference must be a subset, then, of the ideal generated by the largest coefficient. Applying this argument again to $ag_0+bh_0\equiv1\pmod{\mf p}$ and taking the maximum coefficient here (also comparing with $\pi$) then lets us assert simultaneously that\[ag_0+bh_0\equiv1\pmod\pi.\]Essentially, we are attempting to make our ideals principal.
Now let's upgrade $g_0$ and $h_0$ to $g_1$ and $h_1$ to be closer to the desired factorization. We'll take $g_1\equiv g_0\pmod\pi$ and $h_1\equiv h_0\pmod\pi$ and $\deg g_1=\deg g_0,$ and the improvement that we will make is that\[f\equiv g_1h_1\pmod{\pi^2}.\]Then we will be able to rinse and repeat the argument. The argument will be able to port from $\pi$ to $\pi^2$ to an argument to $\pi^3$ and $\pi^4,$ onwards and upwards. The sequence of polynomials $(g_\bullet)$ and $(h_\bullet)$ will converge because they their difference will each be divisible by successively larger powers $\pi^\bullet,$ implying that the difference's coefficients all vanish ($|\pi| \lt 1$); no new terms are created because the degree is kept constant. And further, $g_\bullet h_\bullet$ approaches $f$ for the same reason. So indeed doing this step will complete the proof.
Let's take $g_1=g_0+p_1\pi$ and $h_1=h_0+q_1\pi$ for $p_1,q_1\in\mathcal O_K[x]$ to be fixed later. Observe that\[g_1h_1\equiv g_0+(g_0q_1+h_0p_1)\pi\pmod{\pi^2}.\]In particular, we get to not care about $p_1q_1\pi^2$—we are kind of just looking at the next term in our "power series'' at $\pi.$ Anyways, this is equivalent to\[g_0q_1+h_0p_1\equiv\frac{f-g_0h_0}\pi\pmod\pi.\]To accomplish this, we can use our $a$ and $b.$ In particular, we may take $q_1=b\left(\frac{f-g_0h_0}\pi\right)$ and $p_1=a\left(\frac{f-g_0h_0}\pi\right).$ The degree of $g_1$ might not match now, but we can just reduce $p_1\pmod{g_1}$ to have degree smaller and adjust $q_1$ accordingly. In particular, write\[b\cdot\frac{f-g_0h_0}\pi=g_0q+p_1\]so that $p_1$ has degree smaller than $g_0.$ Now, $g\equiv g_0$ with matching degrees implies that the leading coefficient of $g_0$ has size $1$ and is therefore a unit, so Euclidean division works here; explicitly, $q(x)\in\mathcal O_K[x].$ From this it follows\[g_0\left(a\cdot\frac{f-g_0h_0}\pi+h_0q\right)+h_0p_1\equiv\frac{f-g_0h_0}\pi\pmod{\pi^2}.\]To finish, we check degrees: note $g_1=g_0+\pi p_1$ has the correct degree because $\deg g_0 \gt \deg p_1.$ I guess there is some technicality in checking the degree of $h_1$ does not explode, but it doesn't. We don't deal with that here.