lean_workbook_plus_14094

Proved

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

Prove that for each of the $(1+2x)$ consecutive integers $i$ such that $x^2 \le i < (x+1)^2$ we have $\lfloor\sqrt{i}\rfloor=x$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14094 (x : ℕ) (i : ℕ) (hi : x^2 ≤ i ∧ i < (x + 1)^2) : ⌊Real.sqrt i⌋ = x   :=  by sorry

Source