lean_workbook_plus_24191

Proved

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

Let $a,b\in \mathbb{R}$ and $(a+\sqrt{a^2+1})(b+\sqrt{b^2+1})=k$ , where $k>0.$ Prove that $(1+k)(a+b)=(k-1)(\sqrt{a^2+1}+\sqrt{b^2+1}).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24191 (a b k : ℝ) (h₁ : 0 < k) (h₂ : (a + Real.sqrt (a^2 + 1)) * (b + Real.sqrt (b^2 + 1)) = k) : (1 + k) * (a + b) = (k - 1) * (Real.sqrt (a^2 + 1) + Real.sqrt (b^2 + 1))   :=  by sorry

Source

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

View graph