Prove2Me

lean_workbook_plus_70088

Proved

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

Derive the inequality (a+b)(c+d)≤(a+b+c+d)24(a+b)(c+d)\leq\frac{(a+b+c+d)^2}{4} from the given conditions (a+b)+(c+d)≥2(a+b)(c+d)(a+b)+(c+d)\geq2\sqrt{(a+b)(c+d)}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70088 (a b c d : ℝ) (h : a + b + c + d ≥ 2 * Real.sqrt ((a + b) * (c + d))) :
  (a + b) * (c + d) ≤ (a + b + c + d) ^ 2 / 4   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph