lean_workbook_plus_15603

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Obviously $\boxed{\text{S1 : }f(x)=x^2\text{ }\forall x}$ is a solution. Let us look for other solutions.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_15603 (f : ℝ → ℝ) (hf: f '' Set.univ = Set.univ) (h: ∀ x, f x - x ^ 2 = 0) : ∀ x, f x = x ^ 2   :=  by sorry

Source