lean_workbook_plus_50995

Proved

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

Let $x, y$ be real numbers such that $xy+(x+y)(3-2x-2y)=1.$ Prove that $-1\leq x^2-y^2\leq 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50995 (x y : ℝ) (h : x * y + (x + y) * (3 - 2 * x - 2 * y) = 1) :
  -1 ≤ x^2 - y^2 ∧ x^2 - y^2 ≤ 1   :=  by sorry

Source