Solution (source code)

= Solution

The structural facts used about a non-Archimedean <local field> are that it is complete for a normalized <discrete valuation> $v:K^\times\to\mathbb Z$, its <valuation ring> $\mathcal O_K=\{x:v(x)\ge0\}$ is a <discrete valuation ring>, its maximal ideal is $\mathfrak m_K=\pi\mathcal O_K$ for a <uniformizer> $\pi$, and its <residue field> is a finite field $k=\mathbb F_q$. Polynomial operations are continuous for this valuation topology.

A simple-root version of <Hensel lemma> is: if $f\in\mathcal O_K[X]$, $a_1\in\mathcal O_K$, $f(a_1)\in\mathfrak m_K$, and $f'(a_1)\notin\mathfrak m_K$, then there is a unique $a\in\mathcal O_K$ with $f(a)=0$ and $a\equiv a_1\pmod{\mathfrak m_K}$.

Construct $a_n$ with $f(a_n)\in\pi^n\mathcal O_K$. Given $a_n$, put $a_{n+1}=a_n+\pi^nb_n$. Taylor expansion over the valuation ring gives
$$
f(a_n+\pi^nb_n)\equiv f(a_n)+\pi^nb_nf'(a_n)\pmod{\pi^{n+1}}.
$$
The omitted terms contain $\pi^{2n}$, and $2n\ge n+1$ for $n\ge1$. The residue of $f'(a_n)$ remains the nonzero residue of $f'(a_1)$, so choose $b_n$ with
$$
\overline{b_n}=-\overline{f(a_n)/\pi^n}\,\overline{f'(a_n)}^{-1}.
$$
This makes $f(a_{n+1})\in\pi^{n+1}\mathcal O_K$. The congruences $a_{n+1}\equiv a_n\pmod{\pi^n}$ make $(a_n)$ a <Cauchy sequence>; completeness gives its limit $a\in\mathcal O_K$. Continuity and $v(f(a_n))\ge n$ give $f(a)=0$, and the first congruence gives its specified residue class.

For uniqueness, if $a,b$ are two roots in that class, polynomial division of their difference gives
$$
0=f(a)-f(b)=(a-b)\bigl(f'(b)+(a-b)c\bigr),\qquad c\in\mathcal O_K.
$$
The second factor is a unit, since $f'(b)$ is a unit and $a-b\in\mathfrak m_K$. Thus $a=b$. This proves both existence and uniqueness in the stated <Hensel lemma>.