Prove2Me

lean_workbook_plus_80867

Proved

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

f(x)−f(y)=(ax2+bx+c)−(ay2+by+c)=(x−y)(a(x+y)+b)f\left(x\right)-f\left(y\right)=\left(ax^2+bx+c\right)-\left(ay^2+by+c\right)=\left(x-y\right)\left(a\left(x+y\right)+b\right) ,

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_80867  (a b c x y : ℝ)
  (f : ℝ → ℝ)
  (h₀ : ∀ x, f x = a * x^2 + b * x + c)
  (h₁ : x ≠ y) :
  f x - f y = (x - y) * (a * (x + y) + b)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph