lean_workbook_plus_36737

Proved

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

Set $u=y+z$ then $1\le xu+\frac{u^2}4 \implies x\ge \frac{4-u^2}{4u}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_36737  (x y z u : ℝ)
  (h₀ : 0 < u)
  (h₁ : u = y + z)
  (h₂ : 1 ≤ x * u + u^2 / 4) :
  x ≥ (4 - u^2) / (4 * u)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph