Completing a quadratic square

Proved

WorkbookSource.problem_51317

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

lean-workbooksource-checked

Let's consider $4A^2+8A+1$ alone. Factoring out $4$ gives $4(A^2+2A+1/4)$ . Completing the square: $4(A^2+2A+3/4+1/4)-3=4(A+1)^2-3$

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_51317  (a : ℝ) :
  4 * a^2 + 8 * a + 1 = 4 * (a + 1)^2 - 3  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_51317; Apache-2.0

View graph