simp
case hg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
Ψ : ℝ → ℝ
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
l1 : ContDiff ℝ ⊤ Ψ'
l2 : HasCompactSupport Ψ'
⊢ ∀ {x : ℝ}, ↑x = 0 ↔ x = 0
no goals