simp [Real.fourierChar, expMapCircle, smul_eq_mul, mul_assoc, this]
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
this : ↑n ^ ↑σ' = ↑(↑n ^ σ')
⊢ f n / ↑n ^ ↑σ' * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    (f n * (cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ'))) • ψ y
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
this : ↑n ^ ↑σ' = ↑(↑n ^ σ')
⊢ f n / ↑(↑n ^ σ') * (cexp (-(2 * (↑π * (↑y * ((↑π)⁻¹ * (2⁻¹ * (↑(↑n / x).log * I))))))) * ψ y) =
    f n * (cexp (-(2 * (↑π * (↑y * ((↑π)⁻¹ * (2⁻¹ * (↑(↑n / x).log * I))))))) / ↑(↑n ^ σ') * ψ y)