simp only [RCLike.norm_natCast, Nat.cast_le]
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    ‖↑(Finset.filter IsPrimePow (Finset.range x)).card‖ ≤
      ‖↑(Finset.filter Nat.Prime (Finset.range x) ∪
              Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card‖
case hfg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ (x : ℕ),
    (Finset.filter IsPrimePow (Finset.range x)).card ≤
      (Finset.filter Nat.Prime (Finset.range x) ∪
          Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card