Prove2Me

lean_workbook_plus_64321

Proved

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

Let x,y∈Rx,y \in \mathbb{R} such that ∣x+y∣+∣x−y∣=2.|x+y|+|x-y|=2. Prove that 32≤∣2x−y∣+∣2y−x∣≤6\frac{3}{2}\leq |2x-y|+|2y-x| \leq 6

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

View graph