We say that a polynomial $f(x) ∈ F[x]$ is inseparable if it has a repeated root in some field extension. Otherwise we say that $f(x)$ is separable. Prove that $f(x)$ is separable $\iff\gcd(f, Df) = 1$. Note $Df$ denotes the formal algebraic derivative of $f$.
Instead of proving the bi-conditional as written, I have elected to prove the contrapositive, that is I will prove that $f(x)$ is not separable $\iff\gcd(f, Df)$ is not $1$.
Suppose $f(x) ∈ F[x]$ is inseparable and has degree $n$. Then by definition, $f(x)$ must have a repeated root in some field extension. It is well-known that if $f$ has a repeated root at some $x = a$, $Df$ must also have a root at $x=a$; this follows because we can write $f∈F[x]$ as a product of linear factors in some field extension of $F$ and then apply the product rule for derivatives to find an expression for $Df$ in terms of the linear factors of $f$, which verifies the result above. Hence, $f$ and $Df$ share a common factor, namely $(x-a)^m$, where $m$ is some integer power between $1$ and $n-1$ and thus, $\gcd(f, Df)$ is not equal to $1$.
Conversely, suppose $gcd(f, Df)$ is not equal to $1$. Then it follows that $f$ and $Df$ share a non-trivial common divisor, which without loss of generality, we will call $(x-a)^m$, where $m$ is some integer power between $1$ and $n - 1$. This implies that $Df$ and $f$ share a root at $x = a$ and since $f$ is a polynomial, then $\deg(Df)$ = $n-1 <\deg(f)$ = $n$. In case $m > 1$, it consequently follows that $f$ has a repeated root at $x = a$. Otherwise, if $m = 1$, then both $f$ and $Df$ share the common linear factor $x-a$. However, it is well-known that if $f$ and $Df$ share a root at $x = a$, then $f$ must contain at least one repeated root at $x = a$; this is a consequence that directly follows from the product rule for derivatives. Hence in either case, it follows that $f$ has a repeated root, and thus $f$ is inseparable, as desired.
Your proof of the converse statement is not quite complete; you state that
But you do not explain why this non-trivial common divisor can be assumed to be linear.
Next you claim that
But it is not at all clear (to me, at least) why it follows that $f$ has a repeated root.
My suggestion to improve your proof, is to make explicit your claim that
To prove this, write $f\in F[x]$ as a product of linear factors in some field extension of $F$, and then express $Df$ in terms of the factors of $f$. This expression will make the equivalence you are trying to prove immediately clear.