An equivalent quadratic inequality

Proved

WorkbookSource.problem_242

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

lean-workbooksource-checked

Let $b=a+x, c=a+x+y$ . Then we have $a+a+x \ge a+x+y \implies a\ge y$ . The inequality turns to $(3a+2x+y)^2 \le 9(a+x)(a+x+y)$ $\iff 6(2x+y)a+(2x+y)^2 \le 9a(2x+y)+9x(x+y) \iff 3a(2x+y)+5x^2+5xy \ge y^2$

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_242  (x y a : ℝ) :
  (3 * a + 2 * x + y) ^ 2 ≤ 9 * (a + x) * (a + x + y) ↔ 3 * a * (2 * x + y) + 5 * x ^ 2 + 5 * x * y ≥ y ^ 2  :=  by sorry

Source

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

View graph