lean_workbook_plus_75242

Proved

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

Now ${f(x)=0\implies x^2(x-4)^2-16(2x+1)^2=0\implies (x^2+4x+4)(x^2-12x-4)=0}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75242  (x : ℝ)
  (f : ℝ → ℝ)
  (h₀ : f x = 0)
  (h₁ : f x = (x^2 * (x - 4)^2 - 16 * (2 * x + 1)^2)) :
  x^2 + 4 * x + 4 = 0 ∨ x^2 - 12 * x - 4 = 0   :=  by sorry

Source

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

View graph