[proofplan]
We define $F$ as the set of all elements of $K$ that are separable over $k$, and show it is a subfield (the separable closure of $k$ in $K$). We verify that $F/k$ is separable by construction. The main work is showing $K/F$ is purely inseparable: for each $\alpha \in K$, we use the [Criterion for Inseparability of Irreducible Polynomials](/theorems/3330) to show the minimal polynomial of $\alpha$ over $F$ has the form $x^{p^e} - c$ for some $e \geq 0$ and $c \in F$, which forces $\alpha^{p^e} \in F$. Uniqueness follows from showing that any intermediate field with both properties must equal $F$.
[/proofplan]
[step:Define the separable closure and verify it is a subfield]
Define
\begin{align*}
F := \{\alpha \in K : \alpha \text{ is separable over } k\} = \{\alpha \in K : \operatorname{min}(\alpha, k) \text{ has no repeated roots in } \overline{k}\}.
\end{align*}
We verify $F$ is a subfield of $K$. The elements $0, 1 \in k$ are separable over $k$ (their minimal polynomial is $x$ and $x - 1$, respectively), so $k \subset F$. For closure under field operations: let $\alpha, \beta \in F$, so both are separable over $k$. Consider the extension $k(\alpha, \beta)/k$. Since $\alpha$ is separable over $k$, the extension $k(\alpha)/k$ is separable. Since $\beta$ is separable over $k$, it is also separable over $k(\alpha)$ (the minimal polynomial of $\beta$ over $k(\alpha)$ divides $\operatorname{min}(\beta, k)$, and a divisor of a separable polynomial is separable). By the [Multiplicativity of Separable Degree](/theorems/3331), $k(\alpha, \beta)/k$ is separable. Every element of $k(\alpha, \beta)$ is therefore separable over $k$, and in particular $\alpha + \beta$, $\alpha \beta$, $\alpha - \beta$, and $\alpha / \beta$ (when $\beta \ne 0$) lie in $F$.
[guided]
We set $F$ to be the collection of all elements of $K$ that are separable over $k$. To show $F$ is a subfield, we need closure under addition, subtraction, multiplication, and division.
The key observation is that if $\alpha, \beta \in F$, then $k(\alpha, \beta)/k$ is separable. Here is why. The element $\alpha$ is separable over $k$, so $k(\alpha)/k$ is a separable extension. Now consider $\beta$: it is separable over $k$, meaning its minimal polynomial $m_\beta = \operatorname{min}(\beta, k) \in k[x]$ has no repeated roots. The minimal polynomial of $\beta$ over the larger field $k(\alpha)$ divides $m_\beta$ in $k(\alpha)[x]$ (by the [Properties of the Minimal Polynomial](/theorems/1250), $\operatorname{min}(\beta, k(\alpha)) \mid m_\beta$). Since $m_\beta$ has no repeated roots, neither does any of its divisors. So $\beta$ is separable over $k(\alpha)$, meaning $k(\alpha, \beta) / k(\alpha)$ is separable.
By the [Multiplicativity of Separable Degree](/theorems/3331), $k(\alpha, \beta) / k$ is separable (since both $k(\alpha)/k$ and $k(\alpha, \beta)/k(\alpha)$ are separable). Every element of $k(\alpha, \beta)$ is therefore separable over $k$. Since $\alpha + \beta$, $\alpha - \beta$, $\alpha \beta$, and $\alpha/\beta$ (for $\beta \ne 0$) all belong to $k(\alpha, \beta)$, they lie in $F$. This shows $F$ is a subfield of $K$ containing $k$.
[/guided]
[/step]
[step:Verify that $F/k$ is separable]
By definition, every element of $F$ is separable over $k$. Since $K/k$ is finite, $F/k$ is also finite (as $F \subset K$). A finite extension is separable if and only if every element is separable over the base field, which holds by construction. Hence $F/k$ is separable.
[/step]
[step:Show that $K/F$ is purely inseparable]
We must show that for every $\alpha \in K$, there exists $e \geq 0$ such that $\alpha^{p^e} \in F$, where $p = \operatorname{char}(k)$. (If $\operatorname{char}(k) = 0$, then every algebraic extension is separable, so $F = K$ and $K/F$ is trivially purely inseparable.)
Assume $\operatorname{char}(k) = p > 0$. Let $\alpha \in K$ and let $m = \operatorname{min}(\alpha, F) \in F[x]$ be the minimal polynomial of $\alpha$ over $F$. We claim $m$ is purely inseparable, i.e., $m(x) = (x - \alpha)^d$ in $\overline{k}[x]$ where $d = \deg m$.
Suppose for contradiction that $m$ is separable over $F$. Then $\alpha$ would be separable over $F$. Since $F/k$ is separable and $F(\alpha)/F$ would be separable, the [Multiplicativity of Separable Degree](/theorems/3331) gives $F(\alpha)/k$ separable. But then $\alpha$ is separable over $k$, so $\alpha \in F$ by definition. This means $m = x - \alpha$ has degree $1$, and $\alpha \in F$, which is consistent (but vacuous).
For the general case, suppose $m$ is inseparable. By the [Criterion for Inseparability of Irreducible Polynomials](/theorems/3330), $m(x) = g(x^p)$ for some $g \in F[x]$, since $m$ is irreducible (as a minimal polynomial) and inseparable. Iterating: write $m(x) = h(x^{p^e})$ where $h \in F[x]$ is irreducible and $h'(x) \ne 0$ (choose $e$ maximal so that $m$ can be written as a polynomial in $x^{p^e}$). Then $h$ is separable by the [Criterion for Inseparability of Irreducible Polynomials](/theorems/3330) (since $h$ is irreducible and $h' \ne 0$).
Now $h(\alpha^{p^e}) = m(\alpha) = 0$, so $\alpha^{p^e}$ is a root of the separable irreducible polynomial $h \in F[x]$. Therefore $\alpha^{p^e}$ is separable over $F$. Since $F/k$ is separable and $F(\alpha^{p^e})/F$ is separable, the [Multiplicativity of Separable Degree](/theorems/3331) gives $F(\alpha^{p^e})/k$ separable, so $\alpha^{p^e}$ is separable over $k$, hence $\alpha^{p^e} \in F$.
This shows every $\alpha \in K$ satisfies $\alpha^{p^e} \in F$ for some $e \geq 0$, proving $K/F$ is purely inseparable.
[guided]
We need to show that every element of $K$ has a $p$-power that lands in $F$. If $\operatorname{char}(k) = 0$, every algebraic extension of $k$ is separable (since the formal derivative of an irreducible polynomial of degree $\geq 1$ is nonzero in characteristic $0$), so $F = K$ and $K/F$ is the trivial extension — automatically purely inseparable. The interesting case is $\operatorname{char}(k) = p > 0$.
Fix $\alpha \in K$ and let $m = \operatorname{min}(\alpha, F) \in F[x]$. Since $m$ is the minimal polynomial of $\alpha$ over $F$, it is irreducible in $F[x]$. There are two cases:
**Case 1: $m$ is separable.** Then $\alpha$ is separable over $F$. Since $F/k$ is separable and $F(\alpha)/F$ is separable, the [Multiplicativity of Separable Degree](/theorems/3331) tells us $F(\alpha)/k$ is separable. So $\alpha$ is separable over $k$, meaning $\alpha \in F$. In this case $\alpha^{p^0} = \alpha \in F$, and we are done with $e = 0$.
**Case 2: $m$ is inseparable.** By the [Criterion for Inseparability of Irreducible Polynomials](/theorems/3330), since $m$ is irreducible and inseparable, we have $m(x) = g_1(x^p)$ for some $g_1 \in F[x]$. If $g_1$ is still of the form $g_2(x^p)$, we iterate. After finitely many iterations (the degree drops by a factor of $p$ at each step), we reach
\begin{align*}
m(x) = h(x^{p^e})
\end{align*}
where $h \in F[x]$ is irreducible (it divides $m$ after the substitution, and irreducibility propagates from $m$) and $h$ cannot be written as a polynomial in $x^p$. By the [Criterion for Inseparability of Irreducible Polynomials](/theorems/3330), since $h$ is irreducible and not a polynomial in $x^p$, $h$ must be separable.
Since $m(\alpha) = 0$, we have $h(\alpha^{p^e}) = 0$, so $\alpha^{p^e}$ is a root of the separable irreducible polynomial $h \in F[x]$. Therefore $\alpha^{p^e}$ is separable over $F$. Applying the [Multiplicativity of Separable Degree](/theorems/3331) to the tower $k \subset F \subset F(\alpha^{p^e})$: both $F/k$ and $F(\alpha^{p^e})/F$ are separable, so $F(\alpha^{p^e})/k$ is separable. This means $\alpha^{p^e}$ is separable over $k$, hence $\alpha^{p^e} \in F$ by definition of $F$.
[/guided]
[/step]
[step:Prove uniqueness of the intermediate field]
Let $F'$ be any intermediate field with $k \subset F' \subset K$ such that $F'/k$ is separable and $K/F'$ is purely inseparable. We show $F' = F$.
**$F' \subset F$:** Every element of $F'$ is separable over $k$ (since $F'/k$ is separable), so $F' \subset F$ by definition of $F$.
**$F \subset F'$:** Let $\alpha \in F$, so $\alpha$ is separable over $k$. Since $K/F'$ is purely inseparable, there exists $e \geq 0$ with $\alpha^{p^e} \in F'$ (where $p = \operatorname{char}(k)$; if $\operatorname{char}(k) = 0$, then $K = F'$ and the inclusion is immediate). The minimal polynomial of $\alpha$ over $F'$ divides $x^{p^e} - \alpha^{p^e} = (x - \alpha)^{p^e}$ in $\overline{k}[x]$, so $\operatorname{min}(\alpha, F')$ has $\alpha$ as its only root (possibly with multiplicity). But $\alpha$ is separable over $k$, meaning $\operatorname{min}(\alpha, k)$ is separable. Since $\operatorname{min}(\alpha, F') \mid \operatorname{min}(\alpha, k)$ in $\overline{k}[x]$ (any root of $\operatorname{min}(\alpha, F')$ is a root of $\operatorname{min}(\alpha, k)$, and... more precisely, $\operatorname{min}(\alpha, F')$ divides $\operatorname{min}(\alpha, k)$ in $F'[x]$ since $\operatorname{min}(\alpha, k) \in k[x] \subset F'[x]$ annihilates $\alpha$). A divisor of a separable polynomial is separable, and we showed $\operatorname{min}(\alpha, F')$ has only the root $\alpha$. A separable polynomial with only one distinct root must have degree $1$, so $\operatorname{min}(\alpha, F') = x - \alpha$, giving $\alpha \in F'$.
Therefore $F = F'$.
[guided]
Suppose $F'$ is another intermediate field with $F'/k$ separable and $K/F'$ purely inseparable. We must show $F' = F$.
For the inclusion $F' \subset F$: since $F'/k$ is separable, every $\alpha \in F'$ satisfies that $\operatorname{min}(\alpha, k)$ is separable, so $\alpha \in F$ by definition of $F$.
For the inclusion $F \subset F'$: let $\alpha \in F$. Since $K/F'$ is purely inseparable, $\alpha^{p^e} \in F'$ for some $e \geq 0$. This means $\alpha$ is a root of $x^{p^e} - \alpha^{p^e} \in F'[x]$. In $\overline{k}[x]$, this polynomial factors as $(x - \alpha)^{p^e}$ (using the Frobenius identity $(a - b)^p = a^p - b^p$ in characteristic $p$). So the minimal polynomial $\operatorname{min}(\alpha, F')$ divides $(x - \alpha)^{p^e}$, meaning $\alpha$ is the only root of $\operatorname{min}(\alpha, F')$.
On the other hand, $\operatorname{min}(\alpha, k) \in k[x] \subset F'[x]$ annihilates $\alpha$, so by the [Properties of the Minimal Polynomial](/theorems/1250), $\operatorname{min}(\alpha, F') \mid \operatorname{min}(\alpha, k)$ in $F'[x]$. Since $\alpha \in F$, the polynomial $\operatorname{min}(\alpha, k)$ is separable (no repeated roots). A divisor of a separable polynomial is itself separable (it can only have a subset of the roots, each with multiplicity at most $1$). So $\operatorname{min}(\alpha, F')$ is separable. But we showed it has only the root $\alpha$. A separable polynomial with a single distinct root must be linear: $\operatorname{min}(\alpha, F') = x - \alpha$. This gives $\alpha \in F'$.
[/guided]
[/step]