Prove2Me

lean_workbook_plus_3127

Proved

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

We have this: 2+x2+y21+x2+y2+x2y2≥21+xy⇒(2xy−1)(xy−1)≤0⇔xy∈[12,1]\frac{2+{{x}^{2}}+{{y}^{2}}}{1+{{x}^{2}}+{{y}^{2}}+{{x}^{2}}{{y}^{2}}}\ge \frac{2}{1+xy}\Rightarrow (2xy-1)(xy-1)\le 0\Leftrightarrow xy\in \left[ \frac{1}{2},1 \right]

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3127  (x y : ℝ)
  (h₀ : 0 ≤ 1 + x^2 + y^2 + x^2 * y^2)
  (h₁ : 0 ≤ 2 + x^2 + y^2)
  (h₂ : 1 + x^2 + y^2 + x^2 * y^2 ≠ 0)
  (h₃ : 2 + x^2 + y^2 ≠ 0)
  (h₄ : 0 ≤ x * y) :
  (2 * x * y - 1) * (x * y - 1) ≤ 0 ↔ x * y ∈ Set.Icc (1 / 2) 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph