lean_workbook_plus_36823

Proved

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

Let $x,y \in R$ satisfy $xy+\sqrt{(1+x^2)(1+y^2)}=1$ . Prove that: $x\sqrt{1+y^2}+y\sqrt{1+x^2}=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_36823 (x y : ℝ) (h : x * y + Real.sqrt ((1 + x ^ 2) * (1 + y ^ 2)) = 1) :
  x * Real.sqrt (1 + y ^ 2) + y * Real.sqrt (1 + x ^ 2) = 0   :=  by sorry

Source

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

View graph