Prove2Me

lean_workbook_plus_33273

Proved

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

First equation multiplied by 2 and then added to the second equation leads to:\n

2(x2+2)+2y(y+2x)+y(2x+y)2=22y+2(x2+2)+13y2(x^2+2)+2y(y+2x)+y(2x+y)^2=22y+2(x^2+2)+13y

\n

y[(2x+y)2+2(y+2x)−35]=0y[(2x+y)^2+2(y+2x)-35]=0

\n

y(2x+y+7)(2x+y−5)=0y(2x+y+7)(2x+y-5)=0
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_33273  (x y : ℝ)
  (h₀ : 2 * (x^2 + 2) + 2 * y * (y + 2 * x) + y * (2 * x + y)^2 = 22 * y + 2 * (x^2 + 2) + 13 * y)
  (h₁ : y ≠ 0) :
  (2 * x + y + 7) * (2 * x + y - 5) = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph