have hC_nonneg : 0 ≤ C := by
  have := hC 2
  norm_cast at this
  have hpos : 0 < 2 / Real.log 2 := by positivity
  rw [← mul_le_mul_right hpos]
  linarith
case intro
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)
⊢ cheby fun n => ↑(Λ n)
case intro
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)
hC_nonneg : 0 ≤ C
⊢ cheby fun n => ↑(Λ n)