convert pows_small_primes_le N using 3
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    ↑N ^ 2⁻¹ * (1 + (↑N).log / Real.log 2)

case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤ 1 + (↑N).log / Real.log 2
case h.e'_4.h.e'_5.h.e'_6
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 2⁻¹ = 1 / 2

case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤ 1 + (↑N).log / Real.log 2