Prove2Me

lean_workbook_plus_79055

Proved

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

(x+2)2+(y+2)2≥x+2+y+22\sqrt{(x+2)^2+(y+2)^2}\ge \frac{x+2+y+2}{\sqrt{2}}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_79055 : ∀ x y : ℝ, Real.sqrt ((x + 2) ^ 2 + (y + 2) ^ 2) ≥ (x + 2 + y + 2) / Real.sqrt 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph