change Tendsto (fun x ↦ S x ψ) atTop (𝓝 0)
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
⊢ Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
        ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)))
    atTop (𝓝 0)
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
⊢ Tendsto (fun x => S x ψ.toFun) atTop (𝓝 0)