https://anurudhp.github.io/blogs/lean-functional-equation-proof.html

potw.lean

/- https://leanprover-community.github.io/lean-web-editor -/

import data.real.basic
import init.classical
import algebra.invertible
import algebra.euclidean_domain
import tactic.ring_exp

/- Problem: Find all functions satisfying `prop` -/
def prop (f : ℝ → ℝ) : Prop := 
  ∀ x y : ℝ, f (x * f (y) + f (x)) + f (y * y) = f (x) + y * f (x + y)

/- Verifying some trivial solutions -/
def idf : ℝ → ℝ := λ x, x
example : prop idf :=
begin
  unfold prop idf,
  intros x y,
  ring,
end

def zerof : ℝ -> ℝ := λ x, 0
example : prop zerof :=
begin
  unfold prop zerof,
  intros x y,
  simp,
end

/- Some simple conclusions/results -/
lemma f_0_0__eq__0 : ∀ f, prop f → 
  f (f (0)) = 0 
:= begin
  unfold prop,
  intros f H,
  specialize H 0 0,
  simp at H,
  exact H,
end

lemma f_0__eq__0 : ∀ f, prop f → 
  f (0) = 0
:= begin
  unfold prop,
  intros f H,
  let H01 := H 0 1,
  simp at H01,
  rewrite ← H01,
  apply f_0_0__eq__0,
  exact H,
end

lemma f_x_sq__eq__x_f_x  : ∀ f, prop f → 
  ∀ x, f (x * x) = x * f (x)
:= begin
  unfold prop,
  intros f H x,
  have f0 := f_0__eq__0 f H,
  specialize H 0 x,
  repeat {
    rewrite f0 at H,
    simp at H, 
  },
  exact H
end

lemma f_neg_x__eq__neg_f_x  : ∀ f, prop f → 
  ∀ x, f (- x) = - f (x)
:= begin
  unfold prop,
  intros f H x,
  have fxx1 := f_x_sq__eq__x_f_x f H x,
  have fxx2 := f_x_sq__eq__x_f_x f H (-x),
  simp at *,
  rewrite fxx1 at fxx2,
  cases classical.em (x = 0), {
    rewrite h,
    simp,
    rewrite f_0__eq__0 f H,
    simp,
  }, {
    ring at fxx2,
    have H3 : f (x) * x = -f (-x) * x, { rewrite fxx2, ring },
    have H4 := euclidean_domain.eq_div_of_mul_eq_left h H3,
    rewrite euclidean_domain.mul_div_cancel (-f (-x)) h at H4,
    rewrite H4,
    ring,
  },
end

lemma f_x__eq_f_f_x : ∀ f, prop f → 
  ∀ x, f (f (x)) = f (x)
:= begin
  unfold prop,
  intros f H x,
  have H0 := f_0__eq__0 f H,
  specialize H x 0,
  repeat { simp at H, rewrite H0 at H, simp at H },
  tauto,
end

lemma twice_fy__eq__f_y_minus_x_plus_f_y_plus_x : ∀ f, prop f →
  ∀ x y, 2 * f(y) = f(y - x) + f(y + x)
:= begin
  intros f H x y,
  have Hneg := f_neg_x__eq__neg_f_x f H,
  have Hsq := f_x_sq__eq__x_f_x f H,
  have H0 := f_0__eq__0 f H,

  have H1 := H x y,
  have H2 := H (-x) y,
  have Hadd_eq : (∀ a b c d : ℝ, a = b → c = d → a + c =  b + d), {
    intros a b c d Hab Hcd,
    rewrite Hab, 
    rewrite Hcd,
  },
  ring at H2,
  rewrite Hneg at H2,
  have E : -(x * f y) + -f x = -(x * f y + f x), {ring},
  rewrite E at H2, clear E,
  rewrite Hneg at H2,
  have H3 := Hadd_eq _ _ _ _ H1 H2, clear H1 H2 Hadd_eq,
  ring at H3,
  rewrite Hsq at H3,
  ring at H3,
  cases classical.em (y = 0), {
    -- y = 0
    subst h,
    rewrite H0,
    ring,
    rewrite Hneg,
    ring,
  }, {
    -- y ≠ 0
    have Hcancel := euclidean_domain.eq_div_of_mul_eq_left h H3,
    field_simp at Hcancel,
    rewrite Hcancel,
    ring,
  },
end

lemma f_2x__eq__2_fx : ∀ f, prop f →
  ∀ x, f (2 * x) = 2 * f(x)
:= begin
  intros f H x,
  have h1 := twice_fy__eq__f_y_minus_x_plus_f_y_plus_x f H x x,
  ring at h1,
  rewrite f_0__eq__0 f H at h1,
  ring at h1,
  tauto,
end

lemma f_x_plus_y__eq_fx_plus_fy : ∀ f, prop f → 
  ∀ x y, f (x + y) = f (x) + f (y)
:= begin
  intros f H x y,
  have hf0 := f_0__eq__0 f H,

  have h1 := twice_fy__eq__f_y_minus_x_plus_f_y_plus_x f H ((y - x)/2) ((y + x)/2),
  field_simp at h1,
  ring at h1,
  rewrite ← f_2x__eq__2_fx f H _ at h1,
  ring at h1,
  rewrite add_comm x y,
  exact h1,
end

lemma f_xfy__eq__y_fx : ∀ f, prop f → 
  ∀ x y, f (x * f (y)) = y * f (x)
:= begin
  intros f H x y,
  have Hadd := f_x_plus_y__eq_fx_plus_fy f H,
  have Hidemp := f_x__eq_f_f_x f H,
  have Hsq := f_x_sq__eq__x_f_x f H,
  specialize H x y,
  rewrite Hadd x y at H,
  rewrite Hadd (x * f y) (f x) at H,
  rewrite Hidemp x at H,
  rewrite Hsq y at H,
  have Hcancel : ∀ a b c : ℝ, a + c = b + c → a = b, {
    intros a b c h,
    rewrite eq_add_neg_of_add_eq h,
    ring,
  },
  apply Hcancel (f (x * f(y))) (y * f(x)) (f(x) + y*f(y)),
  ring at *,
  exact H,
end

lemma fx__eq__x_f1 : ∀ f, prop f → 
  ∀ x, f(x) = x * f(1)
:= begin
  intros f H x,
  have H' := f_xfy__eq__y_fx f H 1 x,
  have Hidemp := f_x__eq_f_f_x f H x,
  ring at H',
  rewrite Hidemp at H',
  exact H',
end

lemma f1__eq__0_or_1 : ∀ f, prop f →
  (f(1) = 0) ∨ (f(1)  = 1)
:= begin
  intros f H,
  have Hlinear := fx__eq__x_f1 f H (f(1)),
  have Hidemp := f_x__eq_f_f_x f H 1,
  rewrite Hlinear at Hidemp,
  cases classical.em (f(1) = 0), {
    tauto,
  }, {
    right,
    have H' := @euclidean_domain.eq_div_of_mul_eq_left _ _ (f(1)) (f(1)) (f(1)) h Hidemp,
    field_simp at H',
    exact H',
  }
end

/- Final Solution (Exhaustive) -/
theorem all_solutions : ∀ f, prop f → 
  (∀ x, f(x) = 0) ∨ (∀ x, f(x) = x)
:= begin
  intros f H,
  have Hlinear := fx__eq__x_f1 f H,
  cases f1__eq__0_or_1 f H with Hf1_0 Hf1_1, {
    left,
    intro x,
    rewrite Hlinear,
    rewrite Hf1_0,
    ring,
  }, {
    right,
    intro x,
    rewrite Hlinear,
    rewrite Hf1_1,
    ring,
  },
end