have := Nat.ceil_lt_add_one (show 0 ≤ Real.sqrt N by positivity)
case neg.h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑⌈√↑N⌉₊ - 1 ≤ √↑N
case neg.h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this✝ : 1 ≤ ⌈√↑N⌉₊
this : ↑⌈√↑N⌉₊ < √↑N + 1
⊢ ↑⌈√↑N⌉₊ - 1 ≤ √↑N