lean_workbook_plus_21016

Proved

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

(a) We have $x^2y+y=x^2+x+1\iff (y-1)x^2-x+(y-1)=0$ . Since $x$ is real, its discriminant should be at least $0$ , i.e. $1^2-4(y-1)^2\geq 0\iff4(y-1)^2\leq1\iff-\frac{1}{2} \leq y-1 \leq\frac{1}{2}\iff\frac{1}{2} \leq y \leq\frac{3}{2}.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_21016  (x y : ℝ)
  (h₀ : x^2 * y + y = x^2 + x + 1) :
  1 / 2 ≤ y ∧ y ≤ 3 / 2   :=  by sorry

Source

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

View graph