Prove2Me

lean_workbook_plus_23205

Proved

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

Let f(x)=x2−2 f(x)=x^2-2 . If r r is a root of the equation, then f(r) f(r) must be as well. One case this is possible when f(r)=r  ⟺  (r−2)(r+1)=0 f(r)=r \iff (r-2)(r+1)=0 , or r=2,−1 r=2,-1 . This corresponds to the solutions (4,4),(−2,1) (4,4), (-2,1) .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_23205  (r : ℝ)
  (f : ℝ → ℝ)
  (h₀ : ∀ x, f x = x^2 - 2)
  (h₁ : f r = r) :
  (r - 2) * (r + 1) = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph