simp only [Finset.card_product, Nat.card_Ico, Finset.card_range, Nat.cast_mul, Nat.cast_add,
  Nat.cast_one]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1)).card ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)