Solution (source code)

= Solution

For a finite extension $L/K$ of <local fields>, let $e=e(L/K)$ be its <ramification index> and $f=f(L/K)=[k_L:k_K]$ its <residue-field degree>. An <unramified extension> has $e=1$. A <totally ramified extension> has $e=[L:K]$, equivalently $f=1$. A <tamely ramified extension> has separable residue extension and ramification index coprime to the residue characteristic.

Let $\bar\theta$ generate the finite extension $k_L/k_K$, and let $\bar g$ be its <minimal polynomial>. Lift $\bar g$ to a monic $g\in\mathcal O_K[X]$ and choose any lift $t\in\mathcal O_L$ of $\bar\theta$. Since finite fields are <perfect fields>, $\bar g'(\bar\theta)\ne0$. The simple-root form of <Hensel lemma>, applied inside $L$, gives $\theta\in\mathcal O_L$ with
$$
g(\theta)=0,
\qquad \theta\equiv t\pmod{\mathfrak m_L}.
$$
Set $K_0=K(\theta)$. Its residue field contains $k_K(\bar\theta)=k_L$, so
$$
[K_0:K]\geq[k_L:k_K]=f.
$$
The equation $g(\theta)=0$ gives the reverse inequality. Thus $[K_0:K]=f$, its residue-field degree is $f$, and $e(K_0/K)=1$; hence $K_0/K$ is unramified. Since $k_{K_0}=k_L$, the extension $L/K_0$ has residue-field degree one and is totally ramified. This constructs the <maximal unramified subextension of a local field extension>.