A quadratic inequality on a rectangle

Proved

WorkbookSource.problem_3154

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Suppose $1\le x\le y\le z\le 2$ and denote $u=\frac xz,v=\frac yz\Rightarrow u,v\in\left[\frac 12, 1\right]$ . The inequality becomes $5(u^2+v^2+1)\le 6(u+v+uv)$

Source: InternLM Lean-Workbook, record lean_workbook_3154 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_3154 (u v : ℝ) (hu : 1 / 2 ≤ u ∧ u ≤ 1) (hv : 1 / 2 ≤ v ∧ v ≤ 1) : 5 * (u^2 + v^2 + 1) ≤ 6 * (u + v + u * v)  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_3154; Apache-2.0

View graph