kbuzzard

-- this was compiling with mathlib in June 2020
import tactic

theorem imo2019Q1 (f : ℤ → ℤ) :
(∀ a b : ℤ, f (2 * a) + 2 * (f b) = f (f (a + b))) ↔
(∀ x, f x = 0) ∨ ∃ c, ∀ x, f x = 2 * x + c :=
begin
  split, swap,
  { -- easy way: f(x)=0 and f(x)=2x+c work.
    intro h,