rw [← mul_le_mul_right hpos]
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
this : ↑(Finset.filter IsPrimePow (Finset.range 2)).card ≤ C * (2 / Real.log 2)
hpos : 0 < 2 / Real.log 2
⊢ 0 ≤ C
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
this : ↑(Finset.filter IsPrimePow (Finset.range 2)).card ≤ C * (2 / Real.log 2)
hpos : 0 < 2 / Real.log 2
⊢ 0 * (2 / Real.log 2) ≤ C * (2 / Real.log 2)