[proofplan] A finite extension is Galois if and only if it is both normal and separable. Since $L/K$ is Galois, the extension $L/K$ is normal and separable; we verify that each property passes to $L/F$. For separability, the key observation is that the minimal polynomial of any $\alpha \in L$ over the larger base field $F$ divides the minimal polynomial of $\alpha$ over $K$ inside $F[t]$, and a divisor of a separable polynomial is separable. For normality, the same divisibility relation shows that the minimal polynomial of $\alpha$ over $F$ splits over $L$ whenever the minimal polynomial over $K$ does. [/proofplan]

[step:Reduce to verifying normality and separability of $L/F$ separately] Since $L/K$ is a finite Galois extension, $L/K$ is finite, normal, and separable. The intermediate field $F$ satisfies $K \subset F \subset L$, so $L/F$ is a finite extension (with $[L:F]$ dividing $[L:K]$ by the tower law). To show that $L/F$ is Galois, it suffices to verify that $L/F$ is both normal and separable. [/step]

[step:Establish that the minimal polynomial over $F$ divides the minimal polynomial over $K$]Let $\alpha \in L$ be arbitrary. Denote by $P_{\alpha, K} \in K[t]$ the minimal polynomial of $\alpha$ over $K$, and by $P_{\alpha, F} \in F[t]$ the minimal polynomial of $\alpha$ over $F$. Since $K \subset F$, every polynomial in $K[t]$ is also a polynomial in $F[t]$. In particular, $P_{\alpha, K} \in F[t]$, and $P_{\alpha, K}(\alpha) = 0$. By the defining property of the minimal polynomial, $P_{\alpha, F}$ divides any polynomial in $F[t]$ that has $\alpha$ as a root. Therefore \begin{align*} P_{\alpha, F} \mid P_{\alpha, K} \quad \text{in } F[t]. \end{align*} That is, there exists $q \in F[t]$ such that $P_{\alpha, K} = P_{\alpha, F} \cdot q$.[/step]

[guided]Why does this divisibility hold? The minimal polynomial $P_{\alpha, F}$ is, by definition, the unique monic irreducible polynomial in $F[t]$ having $\alpha$ as a root. A fundamental property of the minimal polynomial is that it divides every polynomial in $F[t]$ that vanishes at $\alpha$. To see this: given any $g \in F[t]$ with $g(\alpha) = 0$, perform the division algorithm in $F[t]$ (which is a Euclidean domain) to write $g = P_{\alpha, F} \cdot q + r$ where $\deg r < \deg P_{\alpha, F}$. Evaluating at $\alpha$ gives $0 = 0 + r(\alpha)$, so $r(\alpha) = 0$. If $r \ne 0$, then $r$ would be a nonzero polynomial of degree strictly less than $\deg P_{\alpha, F}$ vanishing at $\alpha$, contradicting the minimality of $P_{\alpha, F}$. Therefore $r = 0$ and $P_{\alpha, F} \mid g$. Applying this to $g := P_{\alpha, K}$ (which lies in $K[t] \subset F[t]$ and satisfies $P_{\alpha, K}(\alpha) = 0$), we obtain $P_{\alpha, F} \mid P_{\alpha, K}$ in $F[t]$. This divisibility is the engine of the entire proof: both separability and normality of $L/F$ will follow from the corresponding properties of $L/K$ via this relation.[/guided]

[step:Prove that $L/F$ is separable]We must show that for every $\alpha \in L$, the minimal polynomial $P_{\alpha, F}$ has no repeated roots (equivalently, $P_{\alpha, F}$ is separable). Since $L/K$ is separable, $P_{\alpha, K}$ is separable, meaning $P_{\alpha, K}$ has no repeated roots in any extension of $K$ (equivalently, $\gcd(P_{\alpha, K}, P_{\alpha,K}') = 1$ in $K[t]$, where $P_{\alpha,K}'$ denotes the formal derivative). From the previous step, $P_{\alpha, F} \mid P_{\alpha, K}$ in $F[t]$. Every root of $P_{\alpha, F}$ (in an algebraic closure $\bar{F}$) is therefore a root of $P_{\alpha, K}$. Since $P_{\alpha, K}$ has no repeated roots, no root can appear with multiplicity greater than one in $P_{\alpha, K}$, and a fortiori no root can appear with multiplicity greater than one in the divisor $P_{\alpha, F}$. Therefore $P_{\alpha, F}$ is separable. Since $\alpha \in L$ was arbitrary, every element of $L$ has separable minimal polynomial over $F$, so $L/F$ is separable.[/step]

[guided]The argument here relies on a basic fact about polynomials and divisibility of roots. Let us spell it out carefully. Since $L/K$ is separable, $P_{\alpha, K}$ is separable: it has $\deg P_{\alpha, K}$ distinct roots in an algebraic closure $\bar{K}$. We need to show that $P_{\alpha, F}$ is also separable. We know $P_{\alpha, F} \mid P_{\alpha, K}$ in $F[t]$, so we can write $P_{\alpha, K} = P_{\alpha, F} \cdot q$ for some $q \in F[t]$. Suppose for contradiction that $P_{\alpha, F}$ had a repeated root $\beta$ in some extension. Then $(t - \beta)^2 \mid P_{\alpha, F}$ in $\bar{K}[t]$, and since $P_{\alpha, K} = P_{\alpha, F} \cdot q$, we would have $(t - \beta)^2 \mid P_{\alpha, K}$ in $\bar{K}[t]$. This means $\beta$ is a repeated root of $P_{\alpha, K}$, contradicting the separability of $P_{\alpha, K}$. The essential point is that **separability passes to divisors**: a factor of a separable polynomial is separable. This is because the roots of a factor form a subset of the roots of the original polynomial, and a subset of a set of distinct elements consists of distinct elements. Note that the converse need not hold: a factor of an inseparable polynomial can be separable (consider $t^2$ as a factor of $t^2(t-1)$, but that product has distinct roots $0$ and $1$ aside from multiplicity). What matters here is the forward direction: separable polynomial implies separable factors.[/guided]

[step:Prove that $L/F$ is normal]We must show that for every $\alpha \in L$, the minimal polynomial $P_{\alpha, F}$ splits completely over $L$ (that is, all roots of $P_{\alpha, F}$ lie in $L$). Since $L/K$ is normal, $P_{\alpha, K}$ splits completely over $L$: every root of $P_{\alpha, K}$ in an algebraic closure $\bar{K}$ lies in $L$. Write this splitting as \begin{align*} P_{\alpha, K} = (t - \beta_1)(t - \beta_2) \cdots (t - \beta_d) \quad \text{in } L[t], \end{align*} where $d = \deg P_{\alpha, K}$ and each $\beta_i \in L$. From the divisibility $P_{\alpha, F} \mid P_{\alpha, K}$ in $F[t]$, the factorisation above shows that $P_{\alpha, F} \mid (t - \beta_1) \cdots (t - \beta_d)$ in $L[t]$. Since $L[t]$ is a UFD, every monic irreducible factor of $P_{\alpha, F}$ in $L[t]$ must be one of the linear factors $(t - \beta_i)$. Therefore $P_{\alpha, F}$ splits as a product of linear factors over $L$: \begin{align*} P_{\alpha, F} = (t - \beta_{i_1})(t - \beta_{i_2}) \cdots (t - \beta_{i_m}) \end{align*} for some subset $\{i_1, \ldots, i_m\} \subset \{1, \ldots, d\}$, where $m = \deg P_{\alpha, F}$ and each $\beta_{i_j} \in L$. Since $\alpha \in L$ was arbitrary, $L/F$ is normal.[/step]

[guided]The goal is to show that every root of $P_{\alpha, F}$ belongs to $L$. The strategy is to leverage the fact that $P_{\alpha, K}$ already splits over $L$ (by normality of $L/K$) and that $P_{\alpha, F}$ divides $P_{\alpha, K}$. Since $L/K$ is normal, for any $\alpha \in L$, the minimal polynomial $P_{\alpha, K} \in K[t]$ splits completely over $L$. This means we can write \begin{align*} P_{\alpha, K} = (t - \beta_1)(t - \beta_2) \cdots (t - \beta_d) \quad \text{in } L[t], \end{align*} where $d = \deg P_{\alpha, K}$ and every $\beta_i$ belongs to $L$. Now, we established in the previous step that $P_{\alpha, F} \mid P_{\alpha, K}$ in $F[t]$, and hence also in $L[t]$ (since $F \subset L$). The polynomial ring $L[t]$ is a UFD (in fact a PID), and the complete factorisation of $P_{\alpha, K}$ into irreducibles in $L[t]$ is the product of linear factors $(t - \beta_1) \cdots (t - \beta_d)$. Any monic divisor of $P_{\alpha, K}$ in $L[t]$ must therefore be a product of some subset of these linear factors. In particular, $P_{\alpha, F}$ is a product of linear factors $(t - \beta_{i_j})$ with each $\beta_{i_j} \in L$. This means every root of $P_{\alpha, F}$ lies in $L$, so $P_{\alpha, F}$ splits completely over $L$. Why is the divisibility relation so powerful here? Without it, we would need to argue directly that the roots of $P_{\alpha, F}$ lie in $L$ — but $P_{\alpha, F}$ is defined over $F$, not over $K$, so the normality of $L/K$ does not apply to it directly. The divisibility $P_{\alpha, F} \mid P_{\alpha, K}$ bridges this gap: it ensures that the roots of $P_{\alpha, F}$ are a subset of the roots of $P_{\alpha, K}$, and normality of $L/K$ guarantees that all roots of $P_{\alpha, K}$ lie in $L$.[/guided]

[step:Conclude that $L/F$ is Galois] We have verified that the finite extension $L/F$ is both separable (from the third step) and normal (from the fourth step). By the characterisation of Galois extensions, $L/F$ is Galois. [/step]