peel with C N
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|)
case a.h.h
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) ↔
    ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / |(↑N).log|)