lean_workbook_plus_24937

Proved

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

After expanding and rearranging terms we get the equivalent inequality $4x^{2}y^{2}+x^{2}+y^{2}+1\geqslant 6xy.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24937 (x y : ℝ) : 4 * x ^ 2 * y ^ 2 + x ^ 2 + y ^ 2 + 1 ≥ 6 * x * y   :=  by sorry

Source