simp only [isBigO_top, RCLike.norm_natCast, norm_div, Real.norm_eq_abs]
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (∃ C, ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)) ↔
    (fun N => ↑(Finset.filter IsPrimePow (Finset.range N)).card) =O[⊤] fun N => ↑N / (↑N).log
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (∃ C, ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)) ↔
    ∃ C, ∀ (x : ℕ), ↑(Finset.filter IsPrimePow (Finset.range x)).card ≤ C * (↑x / |(↑x).log|)