lean_workbook_plus_49291

Proved

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

Solve for $x$ and $y$ in the equation $a-\sqrt{a^2-1}=x+y-2\sqrt{xy}$ given $a=x+y$ and $a^2-1=4xy$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_49291 (a x y : ℝ) (ha : a = x + y) (hb : a^2 - 1 = 4 * x * y) : a - Real.sqrt (a^2 - 1) = x + y - 2 * Real.sqrt (x * y)   :=  by sorry

Source

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

View graph