[proofplan]
We exhibit a subnormal series with abelian quotients using the ramification filtration $G_{-1} \supseteq G_0 \supseteq G_1 \supseteq \cdots$. First we show the filtration terminates at $\{\mathrm{id}\}$ (since any non-identity automorphism moves some element by a finite amount). Then we show all successive quotients are abelian: $G_{-1}/G_0 \cong \operatorname{Gal}(k_L/k_K)$ is cyclic (as a Galois group of finite fields), and $G_s/G_{s+1}$ injects into the abelian group $U_L^{(s)}/U_L^{(s+1)}$ for $s \geq 0$.
[/proofplan]
[step:Show the ramification filtration terminates at $\{\mathrm{id}\}$]
Recall the ramification groups $G_s = G_s(L/K) = \{\sigma \in \operatorname{Gal}(L/K) : v_L(\sigma(x) - x) \geq s + 1 \text{ for all } x \in \mathcal{O}_L\}$ for $s \geq -1$, with $G_{-1} = \operatorname{Gal}(L/K)$.
We claim $\bigcap_{s \geq -1} G_s = \{\mathrm{id}\}$. Let $\sigma \in \operatorname{Gal}(L/K)$ with $\sigma \neq \mathrm{id}$. Then there exists $x \in \mathcal{O}_L$ with $\sigma(x) \neq x$. Set $N = v_L(\sigma(x) - x) \in \mathbb{Z}_{\geq 0}$ (finite, since $\sigma(x) - x \neq 0$). Then $\sigma \notin G_N$, because $G_N$ requires $v_L(\sigma(y) - y) \geq N + 1$ for all $y \in \mathcal{O}_L$, but $v_L(\sigma(x) - x) = N < N + 1$.
Since $\operatorname{Gal}(L/K)$ is finite (as $L/K$ is a finite extension), the descending chain $G_{-1} \supseteq G_0 \supseteq G_1 \supseteq \cdots$ of subgroups of a finite group must stabilise. Combined with $\bigcap_s G_s = \{\mathrm{id}\}$, there exists $t \geq 0$ such that $G_t = \{\mathrm{id}\}$.
[/step]
[step:Show $G_{-1}/G_0$ is abelian]
By definition, $G_0 = I(L/K)$ is the inertia group. The quotient $G_{-1}/G_0 = \operatorname{Gal}(L/K)/I(L/K)$ is isomorphic to $\operatorname{Gal}(k_L/k_K)$ via the natural restriction map $\sigma \mapsto \bar{\sigma}$ (the induced automorphism of the residue field).
Since $k_K$ is a finite field (as $K$ is a local field), the extension $k_L/k_K$ is a finite extension of finite fields. Every such extension is cyclic: $\operatorname{Gal}(k_L/k_K) \cong \mathbb{Z}/f\mathbb{Z}$ where $f = [k_L:k_K]$, generated by the Frobenius automorphism $x \mapsto x^{|k_K|}$. In particular, $G_{-1}/G_0$ is cyclic, hence abelian.
[/step]
[step:Show $G_s/G_{s+1}$ is abelian for $s \geq 0$]
By the [Quotients of Ramification Groups](/theorems/???), for each $s \geq 0$, the map $\sigma \mapsto \sigma(\pi_L)/\pi_L$ induces an injective group homomorphism
\begin{align*}
G_s/G_{s+1} \hookrightarrow U_L^{(s)}/U_L^{(s+1)}.
\end{align*}
By the [Quotients of Higher Unit Groups](/theorems/???):
- For $s = 0$: $U_L^{(0)}/U_L^{(1)} = U_L/U_L^{(1)} \cong k_L^\times$, which is cyclic (multiplicative group of a finite field), hence abelian.
- For $s \geq 1$: $U_L^{(s)}/U_L^{(s+1)} \cong (k_L, +)$, the additive group of $k_L$, which is abelian.
In both cases, $G_s/G_{s+1}$ injects into an abelian group, so $G_s/G_{s+1}$ is abelian.
[/step]
[step:Conclude solvability of $\operatorname{Gal}(L/K)$]
The chain
\begin{align*}
\operatorname{Gal}(L/K) = G_{-1} \supseteq G_0 \supseteq G_1 \supseteq \cdots \supseteq G_t = \{\mathrm{id}\}
\end{align*}
is a subnormal series (each $G_{s+1}$ is normal in $G_s$ by the [Quotients of Ramification Groups](/theorems/???)) with all successive quotients abelian ($G_{-1}/G_0$ is cyclic, and $G_s/G_{s+1}$ injects into an abelian group for $s \geq 0$). By definition, $\operatorname{Gal}(L/K)$ is solvable.
[guided]
Let us verify this conclusion meets the definition of solvability carefully.
A finite group $\Gamma$ is solvable if and only if there exists a subnormal series
\begin{align*}
\Gamma = N_0 \supseteq N_1 \supseteq \cdots \supseteq N_r = \{e\}
\end{align*}
with each $N_{i+1}$ normal in $N_i$ and each successive quotient $N_i/N_{i+1}$ abelian.
We have constructed exactly such a series. The normality of each $G_{s+1}$ in $G_s$ follows from the [Quotients of Ramification Groups](/theorems/???): each $G_s$ acts on $\pi_L$ by $\sigma \mapsto \sigma(\pi_L)/\pi_L$, and $G_{s+1}$ is the kernel of this action (into $U_L^{(s)}/U_L^{(s+1)}$), hence normal in $G_s$.
The quotients are abelian: $G_{-1}/G_0$ is cyclic (isomorphic to $\operatorname{Gal}(k_L/k_K) \cong \mathbb{Z}/f\mathbb{Z}$), and for $s \geq 0$ each $G_s/G_{s+1}$ is a subgroup of an abelian group ($k_L^\times$ or $(k_L, +)$), hence abelian. Subgroups of abelian groups are abelian.
The series terminates at $\{\mathrm{id}\}$ (as shown in the first step). All three conditions of the definition are satisfied, so $\operatorname{Gal}(L/K)$ is solvable.
Note that this proof does not assume $L/K$ is abelian — it holds for any finite Galois extension of local fields. The solvability comes purely from the ramification filtration structure, which is available for all finite Galois extensions.
[/guided]
[/step]
