IMO 2019 Q1

Determine all functions f : ℤ → ℤ such that, for all integers a and b, f(2a) + 2f(b) = f(f(a+b)).

The desired theorem is that either:

• f = fun _ ↦ 0
• ∃ c, f = fun x ↦ 2 * x + c

Note that there is a much more compact proof of this fact in Isabelle/HOL

• http://downthetypehole.de/paste/4YbGgqb4

theorem imo2019_q1 (f : ℤ → ℤ) : (∀ (a b : ℤ), f (2 * a) + 2 * f b = f (f (a + b))) ↔ f = 0 ∨ ∃ (c : ℤ), f = fun (x : ℤ) => 2 * x + c