Prove2Me

Simplifying a polynomial expression

Proved
WorkbookSource.problem_26577

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

f(x)=x2+(x2−1)+(2−2x)+2x−7=2x2−6 f(x)=x^{2}+(x^{2}-1)+(2-2x)+2x-7=2x^{2}-6

Source: InternLM Lean-Workbook, record lean_workbook_26577 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_26577 (x : ℝ) : x^2 + (x^2 - 1) + (2 - 2*x) + 2*x - 7 = 2*x^2 - 6  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_26577; Apache-2.0

View graph