Prove2Me

lean_workbook_plus_78918

Proved

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

By Cauchy-Schwartz, 1x+y+1x+z≥42x+y+z\frac {1}{x+y}+\frac {1}{x+z}\ge \frac{4}{2x+y+z}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_78918 {x y z : ℝ} (hx : x > 0) (hy : y > 0) (hz : z > 0) : (1 / (x + y) + 1 / (x + z)) ≥ 4 / (2 * x + y + z)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph