lean_workbook_plus_5335

Proved

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

Prove that $\frac{(x+1)(y+1)(xy+1)}{(x^2+1)(y^2+1)}\leq 2$ where $x$ and $y$ are real numbers

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source