lean_workbook_plus_10779
Proved@ above: which gives . This factors out as .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10779 (x : ℝ) : 64 * (x^2 + 4 * x + 4) * (1 - x) = (x^2 - 22 * x + 121) * (x + 1) ↔ 65 * x^3 + 171 * x^2 + 99 * x - 135 = 0 := by sorry
Source