rw [← Real.sqrt_eq_rpow, Nat.cast_sub this, Nat.cast_one]
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 ^ (1 / 2)
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