Prove2Me

lean_workbook_plus_17220

Proved

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

prove that: a(c−d)(ac−b2−ad+cd)+b(d−a)(ad−c2−ab+bd)+c(a−b)(ab−d2−bc+ac)+d(b−c)(bc−a2−cd+bd)=1/4(ab−ad−bc+ac−bd+cd)2+1/8(b−d)2(a−c)2+3/4(bd−ac)2+3/4(ac−bd)2+1/4(ad−ab−ac+bc−cd+bd)2+1/8(−a+c)2(b−d)2+1/8(−b+d)2(−a+c)2+1/8(a−c)2(−b+d)2,a(c-d)(ac-b^2-ad+cd)+b(d-a)(ad-c^2-ab+bd)+c(a-b)(ab-d^2-bc+ac)+d(b-c)(bc-a^2-cd+bd) = 1/4(ab-ad-bc+ac-bd+cd)^2+1/8(b-d)^2(a-c)^2+3/4(bd-ac)^2+3/4(ac-bd)^2+1/4(ad-ab-ac+bc-cd+bd)^2+1/8(-a+c)^2(b-d)^2+1/8(-b+d)^2(-a+c)^2+1/8(a-c)^2(-b+d)^2,

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_17220 (a b c d : ℝ) :
  a * (c - d) * (a * c - b ^ 2 - a * d + c * d) + b * (d - a) * (a * d - c ^ 2 - a * b + b * d) + c * (a - b) * (a * b - d ^ 2 - b * c + c * a) + d * (b - c) * (b * c - a ^ 2 - c * d + d * b) =
  1 / 4 * (a * b - a * d - b * c + c * a - b * d + d * c) ^ 2 + 1 / 8 * (b - d) ^ 2 * (a - c) ^ 2 + 3 / 4 * (b * d - a * c) ^ 2 + 3 / 4 * (a * c - b * d) ^ 2 + 1 / 4 * (a * d - a * b - a * c + b * c - c * d + b * d) ^ 2 + 1 / 8 * (-a + c) ^ 2 * (b - d) ^ 2 + 1 / 8 * (-b + d) ^ 2 * (-a + c) ^ 2 + 1 / 8 * (a - c) ^ 2 * (-b + d) ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph