Prove2Me

lean_workbook_plus_5232

Proved

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

In the first, ∣x−y∣=∣(2x+y)−(x+2y)∣≤∣2x+y∣+∣x+2y∣|x-y|=|(2x+y)-(x+2y)|\le |2x+y|+|x+2y| .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_5232 (x y : ℝ) : |x - y| ≤ |2 * x + y| + |x + 2 * y|   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph