import Mathlib.Tactic

/-!
# International Mathematical Olympiad 2015, Problem 5

Determine all functions f : ℝ → ℝ that satisfy

  f(x + f(x + y)) + f(xy) = x + f(x + y) + yf(x)

for all x,y.
-/

namespace Imo2012P5

/- determine -/ abbrev solution_set : Set (ℝ → ℝ) := sorry

theorem imo2015_p5 (f : ℝ → ℝ) :
    f ∈ solution_set ↔
    ∀ x y, f (x + f (x + y)) + f (x * y) = x + f (x + y) + y * f x := sorry

This problem does not yet have a complete solution.