lean_workbook_plus_52211

Proved

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

Prove that $\frac{1}{x^2+1}+\frac{1}{y^2+1}\geq \frac{2}{1+xy}$ when $xy\geq 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_52211 (x y : ℝ) (h : x * y ≥ 1) :
  1 / (x ^ 2 + 1) + 1 / (y ^ 2 + 1) ≥ 2 / (1 + x * y)   :=  by sorry

Source