lean_workbook_plus_52010

Proved

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

Prove that for real numbers $x$ and $y$ , we have $\left(xy+x+y-1\right)^2\leq2\left(x^2+1\right)\left(y^2+1\right).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_52010 (x y : ℝ) :
  (x * y + x + y - 1) ^ 2 ≤ 2 * (x ^ 2 + 1) * (y ^ 2 + 1)   :=  by sorry

Source