Prove2Me

A cancellation identity for six real variables

Proved
WorkbookSource.problem_6696

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

lean-workbooksource-checked

prove: ((b−a)(d−c)(f−e)−(b−c)(d−e)(f−a))+((b−c)(a−e)(f−d)+(c−a)(e−f)(d−b))=0 \left ( (b - a)(d - c)(f - e) - (b - c)(d - e)(f - a) \right ) + \left ( (b - c)(a - e)(f - d) + (c - a)(e - f)(d - b) \right ) = 0

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_6696 (a b c d e f : ℝ) : (b - a) * (d - c) * (f - e) - (b - c) * (d - e) * (f - a) + (b - c) * (a - e) * (f - d) + (c - a) * (e - f) * (d - b) = 0  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_6696; Apache-2.0

View graph