Prove2Me

lean_workbook_plus_1554

Proved

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

Let x=a2,1−x=b2x=a^2, 1-x=b^2 . We get ab(a+1+a2)≤1ab(a+\sqrt{1+{{a}^{2}}})\le 1 and a2+b2=1{{a}^{2}}+{{b}^{2}}=1 so 1+a2≤1−a2bab⇒a2b2+2a2b−1≤0\sqrt{1+{{a}^{2}}}\le \frac{1-{{a}^{2}}b}{ab}\Rightarrow {{a}^{2}}{{b}^{2}}+2{{a}^{2}}b-1\le 0 and replacing a2=1−b2⇒b4+2b3−b2−2b+1≥0⇔(b2+b−1)2≥0{{a}^{2}}=1-{{b}^{2}}\Rightarrow {{b}^{4}}+2{{b}^{3}}-{{b}^{2}}-2b+1\ge 0\Leftrightarrow {{({{b}^{2}}+b-1)}^{2}}\ge 0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1554  (a b : ℝ)
  (h₀ : 0 < a ∧ 0 < b)
  (h₁ : a * b * (a + Real.sqrt (1 + a^2)) ≤ 1)
  (h₂ : a^2 + b^2 = 1) :
  Real.sqrt (1 + a^2) ≤ (1 - a^2 * b) / (a * b)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph