lean_workbook_plus_66080

Proved

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

$a+b=c+d \implies a-c=d-b \implies a^2-2ac+c^2=d^2-2bd+b^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_66080 {a b c d : ℝ} (habc : a + b = c + d) (hab : a - c = d - b) : a^2 - 2 * a * c + c^2 = d^2 - 2 * b * d + b^2   :=  by sorry

Source

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

View graph