How can I solve the functional equation
$$f(x + f(x+y)) = x + f(f(x) + y)$$
where $f : \mathbb{R} \to \mathbb{R}$?
I immediately see that the result must be of the form $f(x) = x + C = x + f(0)$
I also noticed that I can use the following:
$$y = -f(x) \implies f(x + f(x-f(x))) = x + f(0)$$ $$y = 0 \implies f(x + f(x)) = x + f(f(x))$$ $$x = 0 \implies f(f(y)) = f(f(0)+y)$$ $$y = -x \implies f(x + f(0)) = x + f(f(x) - x)$$ $$x = -y \implies f(-y + f(0)) = -y + f(f(-y) + y)$$
and in particular
$$f(x) = x - f(0) +f(f(x - f(0)) - x + f(0))$$
But I could not prove the statement. What did I miss?
Introduction
This is an olympiad problem. Typically, these problems require ad-hoc techniques, but in generality, one sees a few patterns such as injectivity, monotonicity and brute force plugging in of obvious values, which allow us to derive some basic identities from which we can work.
In this case, the observation I made was something interesting. While I wasn't quite getting injectivity everywhere (which would very easily finish the problem!) , surjectivity was not a problem at all.
Then, using a preimage of $0$, I observed that an iterated identity (the "$x=0$" case above) was very interesting because I could now apply $f$ to an equation many times and obtain more identities. However, that bit of insight only arose overnight, so you're seeing about $3$ hours of combined effort condensed into one small post.
Let me begin with notation.
Notation
Just tagging some of the equations just like the OP did so. We'll use all of them except for the last two, which turn out to not be useful.
\begin{gather} f(x+f(x+y)) = x+f(f(x)+y) \tag{OG} \\ f(x+f(x-f(x))) = x+f(0) \tag{$y = -f(x)$} \\ f(x+f(x)) = x+f(f(x))\tag{$y=0$} \\ f(f(y)) = f(f(0)+y)\tag{$x=0$} \\ \end{gather}
Polishing the easy part off now.
Surjectivity of $f$
Note that by the condition ($y = -f(x)$), we see that $x+f(0)$ lies in the range of $f$ for every $x \in \mathbb R$. However, $x+f(0)$ spans all the real numbers for $x \in \mathbb R$, therefore $f$ has range $\mathbb R$, hence is surjective. In particular, there is at least one value $X$ such that $f(X)=0$.
$X$ is , in fact, unique : and what it is, is surprising
Let $X$ be any value such that $f(X) =0$. Then, substitute $x=X$ in the equation ($y=0$) : $$ f(X+f(X)) = X+f(f(X)) \implies 0 = X+f(0) \implies X = -f(0) $$
For free, we have obtained that $X$ is , in fact , a unique quantity. Let us now revisit the equation ($x=0$). That is, $$f(f(y)) = f(f(0)+y)$$ for all $y$. Let $X+z = y$,so that $$f(f(X+z)) = f(f(0)+X+z) = f(z) \tag{IMP}$$ for all $z$. (IMP) stands for important!
This took a whole day to come up with, and still looks magical
Let us now set $x=X$ in $(OG)$, so that $$X+f(y) = f(X+f(X+y))$$
For all the equations which try to iterate $f$, it felt sensible to apply $f$ to both sides here, so that $$f(X+f(y)) = f(f(X+f(X+y)))$$
Observe that $f(f(X+f(X+y))) = f(f(X+K))$ where $K = f(X+y)$. Therefore, by using $(IMP)$ twice, we get $$ f(f(X+f(X+y))) = f(f(X+K)) \underbrace{=}_{(IMP)} f(K) = f(f(X+y)) \underbrace{=}_{(IMP)} f(y) $$
That is, we have proved that $$ f(X+f(y)) = f(y) $$
for all $y$. However, $f$ is surjective! Therefore, we have obtained that $f(X+z) = z$ for all $z \in \mathbb R$ by surjectivity, because $f(y)$ spans all real numbers.
A simple rewrite of the form $y = X+z$ reveals that $f(y) = y-X$ for all real numbers $y$. However, $X$ can be arbitrarily chosen : that much is clear by substitution.
Hence, we obtain that $f(y) = y+C$ for $C \in \mathbb R$ arbitrary is the set of all solutions. The key idea was the iteration of $f$, and some observations around $X$.