lean_workbook_plus_74894

Proved

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

So $40x+20727\ge 2(8x^2+4x+3)+1$ , which is $x^2-2x-1295\le 0$ and so $x\in[1,37]$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_74894  (x : ℕ)
  (h₀ : 0 < x)
  (h₁ : 40 * x + 20727 ≥ 2 * (8 * x^2 + 4 * x + 3) + 1) :
  1 ≤ x ∧ x ≤ 37   :=  by sorry

Source