lean_workbook_plus_9879

Proved

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

Put $u:=\sqrt{2x+19}\implies 2x=u^2-19$ , hence the equation becomes \n \n $2u^2-14[u]+21=0\iff u^2-7[u]+{21\over 2}=0$ \n

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9879  (x : ℝ)
  (u : ℝ)
  (h₀ : 0 ≤ 2 * x + 19)
  (h₁ : u = Real.sqrt (2 * x + 19))
  (h₂ : 2 * u^2 - 14 * u + 21 = 0) :
  u^2 - 7 * u + 21 / 2 = 0   :=  by sorry

Source

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

View graph