lean_workbook_plus_60705

Proved

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

((3xy)^2+4)/(xy)>12\n(assuming x and y are both positive)\nWe have $9x^2y^2-12xy+4 \ge 0$ or $(3xy-2)^2 \ge 0$ , true by the trivial inequality

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60705  (x y : ℝ)
  (h₀ : 0 < x ∧ 0 < y) :
  9 * x^2 * y^2 - 12 * x * y + 4 ≥ 0   :=  by sorry

Source