lean_workbook_plus_61733

Proved

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

Let $a=x^2+4x+8$ , then $\frac {1}{\sqrt{x^2+4x+13}+\sqrt{x^2+4x+8}}=\frac{1}{10}\iff \frac{1}{\sqrt a+\sqrt{a+5}}=\frac{1}{10}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_61733 (x : ℝ) (a : ℝ) (ha : a = x^2 + 4*x + 8) : (1 / (Real.sqrt (x^2 + 4*x + 13) + Real.sqrt (x^2 + 4*x + 8))) = 1 / 10 ↔ (1 / (Real.sqrt a + Real.sqrt (a + 5))) = 1 / 10   :=  by sorry

Source

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

View graph