Prove2Me

lean_workbook_plus_11938

Proved

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

Let a=x−y,b=y−z,c=z−xa=x-y , b=y-z , c=z-x , then we are given that \n a2+b2+c2=(a−b)2+(b−c)2+(c−a)2⇒a2+b2+c2−2ab−2bc−2ca=0a^2 + b^2 + c^2 = (a-b)^2 + (b-c)^2 + (c-a)^2 \Rightarrow a^2+ b^2+c^2 -2ab - 2bc - 2ca = 0 but as a+b+c=0⇒2(ab+bc+ca)=−(a2+b2+c2)a+b+c=0 \Rightarrow 2(ab+bc+ca) = - (a^2+b^2+c^2) , so \n a2+b2+c2−2ab−2bc−2ca=0⇒a2+b2+c2=0⇒a=b=c=0a^2+ b^2+c^2 -2ab - 2bc - 2ca = 0 \Rightarrow a^2 + b^2 + c^2 = 0 \Rightarrow a=b=c=0 ⇒x=y=z\Rightarrow x=y=z

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_11938  (x y z : ℝ)
  (h₀ : x - y = z - x)
  (h₁ : y - z = x - y)
  (h₂ : x - y + y - z + z - x = 0) :
  x - y = 0 ∧ y - z = 0 ∧ z - x = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph