Prove2Me

lean_workbook_plus_73131

Proved

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

Solve the system of equation\n\n {x+y+z+u=5(1)y+z+u+v=1(2)z+u+v+x=2(3)u+v+x+y=0(4)v+x+y+z=4(5)\left\{\begin{array}{l}x+y+z+u=5(1)\\y+z+u+v=1(2)\\z+u+v+x=2(3)\\u+v+x+y=0(4)\\v+x+y+z=4(5)\\ \end{array}\right.\n\nLet a=x+y,b=z+ua=x+y,b=z+u \n\n (1):a+b=5(I)(1) :a+b=5(I) \n\n (2)+(3):a+2b+2v=3(II)(2)+(3):a+2b+2v=3(II) \n\n (4)+(5):2a+b+2v=4(III)(4)+(5):2a+b+2v=4(III) \n\n (I),(II),(III)(I),(II),(III) \n\n {a+b=5a+2b+2v=32a+b+2v=4\left\{\begin{array}{l}a+b=5\\a+2b+2v=3\\2a+b+2v=4\\ \end{array}\right.\n\n a=3,b=2,v=−2a=3,b=2,v=-2 \n\n (3)−(2):x−y=1(3)-(2):x-y=1 \n\n {x+y=a=3x−y=1\left\{\begin{array}{l}x+y=a=3\\x-y=1\\ \end{array}\right.\n\n x=2,y=1x=2,y=1 \n\n (5)−(4):z−u=4(5)-(4):z-u=4 \n\n {z+u=b=2z−u=4\left\{\begin{array}{l}z+u=b=2\\z-u=4\\ \end{array}\right.\n\n z=3,u=−1z=3,u=-1 \n\nSo x=2,y=1,z=3,u=−1,v=−2x=2,y=1,z=3,u=-1,v=-2

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_73131  (x y z u v : ℝ)
  (h₀ : x + y + z + u = 5)
  (h₁ : y + z + u + v = 1)
  (h₂ : z + u + v + x = 2)
  (h₃ : u + v + x + y = 0)
  (h₄ : v + x + y + z = 4) :
  x = 2 ∧ y = 1 ∧ z = 3 ∧ u = -1 ∧ v = -2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph