convert tmp N using 4 <;> norm_num
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.filter Nat.Prime (Finset.range N)).card ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ 2⁻¹ * (1 + 2⁻¹ * (↑N).log) ^ 3)

case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ 2⁻¹ * (1 + 2⁻¹ * (↑N).log) ^ 3)
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ 0 ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ 2⁻¹ * (1 + 2⁻¹ * (↑N).log) ^ 3)