apply eventually_of_forall
case intro.refine_2
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
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝 1,
    x_1 ∈ Ioi 1 →
      ∀ (k : ℕ),
        ‖term f (↑x_1) k * 𝓕 ψ.toFun (1 / (2 * π) * (↑k / x).log)‖ ≤
          ‖f k‖ / ↑k * (C / (1 + (1 / (2 * π) * (↑k / x).log) ^ 2))
case intro.refine_2.hp
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
⊢ ∀ x_1 ∈ Ioi 1,
    ∀ (k : ℕ),
      ‖term f (↑x_1) k * 𝓕 ψ.toFun (1 / (2 * π) * (↑k / x).log)‖ ≤
        ‖f k‖ / ↑k * (C / (1 + (1 / (2 * π) * (↑k / x).log) ^ 2))