lean_workbook_plus_44396

Proved

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

As said in the previous comments we can easily see that $f(0)=0$ and $f(x)(f(x)-x)=0$ for all $x$ . Denote: $A=\left\{ x \in R : f(x) = 0 \right\}$ and $B=\left\{ x \in R-{0} : f(y) = y \right\}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_44396  (f : ℝ → ℝ)
  (h₀ : ∀ x, (x = 0 ∨ f x * (f x - x) = 0)) :
  ∀ x, (x = 0 ∨ f x = 0) ∨ f x = x   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph