lean_workbook_plus_75011

Proved

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

It suffices to prove that $(x+y)^{2}\ge 4xy$ and $(x+z)^{2}\ge 4xz$ <=> $(x-y)^{2}\ge 0$ and $(x-z)^{2}\ge0$ It is true

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75011 (x y z : ℝ) : (x + y) ^ 2 ≥ 4 * x * y ∧ (x + z) ^ 2 ≥ 4 * x * z ↔ (x - y) ^ 2 ≥ 0 ∧ (x - z) ^ 2 ≥ 0   :=  by sorry

Source