simp [term, hn]
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : n = 0
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))

case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))