lean_workbook_plus_3470

Proved

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

Replace $x+3$ with $z$ . Now we have $f(z)=3(z-3)^2+7(z-3)+4=3z^2-18z+27+7z-21+4=3z^2-11z+10$ . Because this holds for all reals, we can simply substitute $x$ for $z$ again to get $f(x)=y=3x^2-11x+10$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3470  (x y : ℝ)
  (f : ℝ → ℝ)
  (h₀ : ∀ z, f z = 3 * (z - 3)^2 + 7 * (z - 3) + 4)
  (h₁ : y = f x) :
  y = 3 * x^2 - 11 * x + 10   :=  by sorry

Source

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

View graph