lean_workbook_plus_7451

Proved

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

Therefore, we have $x+\sqrt{x^2+1}-(x-\sqrt{x^2+1})=2\sqrt{x^2+1}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7451  (x : ℝ) :
  x + Real.sqrt (x^2 + 1) - (x - Real.sqrt (x^2 + 1)) = 2 * Real.sqrt (x^2 + 1)   :=  by sorry

Source