lean_workbook_plus_5971

Proved

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

$- \left( b+d \right) \left( c+a \right) \left( acd+abd+abc+bcd \right) + \left( a+b+c+d \right) \left( ab+cd \right) \left( bc+ad \right) = \left( a-c \right) ^{2}bcd+ \left( b-d \right) ^{2}acd+ \left( c-a \right) ^{2}abd+ \left( d-b \right) ^{2}abc$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_5971 (a b c d : ℝ) :
  -(b + d) * (c + a) * (a * c * d + a * b * d + a * b * c + b * c * d) + (a + b + c + d) * (a * b + c * d) * (b * c + a * d) =
  (a - c) ^ 2 * b * c * d + (b - d) ^ 2 * a * c * d + (c - a) ^ 2 * a * b * d + (d - b) ^ 2 * a * b * c   :=  by sorry

Source

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

View graph