Prove2Me

lean_workbook_plus_50476

Proved

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

f(x)=2023xf(x)=2023x ∀x≤−1\forall x\le -1 and f(x)=−2022x2−1f(x)=-2022x^2-1 ∀x>−1\forall x>-1

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_50476 (x : ℝ) (f : ℝ → ℝ) (hf: f = fun x => if x ≤ -1 then 2023 * x else -2022 * x ^ 2 -1) : ∃ x, ∃ y, x < y ∧ f x = f y   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph