Prove2Me

lean_workbook_plus_60869

Proved

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

Let x=1,y=1,z=1x=1, y=1, z=1 and you get that the inequality has to be bounded by 1212 . We can see that ∣1+y∣+∣1+z∣+∣x+y∣+∣y+z∣+∣z+x∣≤12\mid1+y\mid+\mid1+z\mid+\mid x+y\mid+\mid y+z\mid+\mid z+x\mid\leq12 by a simple application of the triangle inequality: ∣1+y∣+∣1+z∣+∣x+y∣+∣y+z∣+∣z+x∣≤3+3∣x∣+3∣y∣+3∣z∣=12.\mid1+y\mid+\mid1+z\mid+\mid x+y\mid+\mid y+z\mid+\mid z+x\mid\leq 3+3\mid x\mid+3\mid y\mid+3\mid z\mid=12.

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

View graph