have l1 : 0 < (n : ℝ) := by simpa using Nat.pos_iff_ne_zero.mpr hn
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)