Prove2Me

lean_workbook_plus_5776

Proved

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

xyz=(1−x)(1−y)(1−z)→2xyz+x+y+z=xy+yz+zx+1 xyz = (1 - x)(1 - y)(1 - z)\rightarrow 2xyz + x + y + z = xy + yz + zx + 1

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_5776 (x y z : ℂ) (h : x * y * z = (1 - x) * (1 - y) * (1 - z)) :
  2 * x * y * z + x + y + z = x * y + y * z + z * x + 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph