lean_workbook_plus_25993

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) -4\, \left( a+b+c+d \right) abcd= \left( b-d \right) ^{2}{a}^{2}c+ \left( a-c \right) ^{2}b{d}^{2}+ \left( d-b \right) ^{2}{c}^{2}a+ \left( c-a \right) ^{2}{b}^{2}d$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source

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

View graph