lean_workbook_plus_80941

Proved

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

Prove that for real numbers $x, y$ with $|x| \leq 1$ and $|y| \leq 1$ , the following equality holds:\n $x^2 + y^2 - 2x^2y^2 + 2xy\sqrt{1-x^2}\sqrt{1-y^2} = (x\sqrt{1-y^2} + y\sqrt{1-x^2})^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_80941 (x y : ℝ) (hx : abs x ≤ 1) (hy : abs y ≤ 1) : x^2 + y^2 - 2 * x^2 * y^2 + 2 * x * y * Real.sqrt (1 - x^2) * Real.sqrt (1 - y^2) = (x * Real.sqrt (1 - y^2) + y * Real.sqrt (1 - x^2))^2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph