congr with n
case e_f.h
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    ∑' (z : ℕ), term f (↑σ' + ↑y * I) z • (ψ y * ↑x ^ (↑y * I))
case e_f.h.e_f.h
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))