Derivative of an algebraic generator lies in the extension

Let $G$ be a field of characteristic zero with a derivation $D$, let $F\subseteq G$ be a subfield, and let $K$ be an intermediate field $F\subseteq K\subseteq G$ with $D(K)\subseteq K$. Let $t\in G$ be algebraic over $K$. Then the derivative of $t$ lies in the field generated by $K$ and $t$:

Together with the logarithmic and exponential generators ($Dt=Ds/s$, respectively $Dt=t\,Ds$, with $s\in K$), this shows that every step of an elementary tower of intermediate fields of a differential field $G$ is closed under $D$, so the tower consists of differential subfields of $G$.

Formalization Note Only a derivation on $G$ is assumed; the base field $F$ carries no differential structure here. The field $K(t)$ is IntermediateField.adjoin F (insert t K).