apply Tendsto.mul_const
case intro.refine_1
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
n : ℕ
⊢ Tendsto (fun x_1 => term f (↑x_1) n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)))
case intro.refine_1.h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
n : ℕ
⊢ Tendsto (fun k => term f (↑k) n) (𝓝[>] 1) (𝓝 (f n / ↑n))