have : 1 ≤ Nat.ceil (Real.sqrt N) := by
  simp only [Nat.one_le_ceil_iff, Real.sqrt_pos, Nat.cast_pos]
  omega
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)