lean_workbook_plus_61046

Proved

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

Find the maximum possible value of \n $\dfrac{(x-y)(1-xy)}{(1+x^2)(1+y^2)}$ \n for real numbers $x$ and $y$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source