Showing that for $f \in K[x]$, we have $f(x) \mid f(x + f(x))$

Another way of saying that $f(x)|f(x+f(x))$ is that $f(x+f(x))$ belongs to the ideal $(f(x))$ generated by $f(x)$ in $K[x]$. At the same time this is equivalent to $\pi(f(x+f(x))=\overline{f(x+f(x))}=0$, where $\pi$ is the natural quotient homomorphism $$\pi:K[x]\to K[x]/(f(x)).$$ Now you're done cause $$\overline{f(x+f(x))}=f(\overline{x}+\overline{f(x)})=f(\overline{x})=0.$$

Note that $(x+y)^j = x^j + y p_j(x,y)$ for some polynomial $p_j(x,y)$. With $y = f(x)$ you get $(x+y)^j = x^j + f(x) p_j(x,f(x))$.

Now when you consider $f(x+f(x))$ use this. Collecting all the terms corresponding to the $x^j$ together yields just $f(x)$, while all the rest is clearly divisible by $f(x)$ as each summand was of the form $f(x)$ "times something."

Note though that your formula for $f(x + f(x))$ is not quite correct. It is $f(f(x))$ that you write down.

Let $ L = K(c_0, c_1, \ldots, c_n) $ be an extension of $ K $ by $ n+1 $ indeterminates, and consider the element $ g(x) = \sum c_k x^k $ in $ L[x] $. Let $ \bar{L} $ denote the splitting field of $ g $ over $ L $. It is clear that $ g $ has distinct roots in $ \bar{L} $, as otherwise no polynomial of degree $ n $ in $ K[x] $ could have distinct roots, and we can always produce a polynomial which will (why?). Now, for any root $ \alpha \in L $ of $ g $ we have that $ g(\alpha + g(\alpha)) = g(\alpha) = 0 $, so that $ (x - \alpha) | g(x + g(x)) $, and as $ g(x) $ has distinct roots this implies $ g(x + g(x)) = g(x) q(x) $ for some $ q \in L[x] $.

Now, let $ f = \sum a_k x^k \in K[x] $, and let $ \phi : L \to K $ be an evaluation map fixing $ K $ and sending $ c_k \to a_k $. Extending it to a map $ \varphi : L[x] \to K[x] $ by acting on the coefficients, we have

$$ f(x + f(x)) = \varphi( g(x + g(x)) ) = \varphi ( g(x) ) \varphi(q(x)) = f(x) q'(x) $$

for some $ q' \in K[x] $, and the proof is complete.

The essence of this proof is to first prove the given property for a generic polynomial, which has the nice property of having distinct roots; and then use this to deduce that the property must hold for any specific polynomial.