simp [Real.fourierChar, expMapCircle, mul_comm (f _)]
case h.e'_3.h.e_f.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ f x✝ * cexp (↑x✝¹.log * ↑x✝ * I) = 𝐞 (-((innerₗ ℝ) x✝) (-x✝¹.log / (2 * π))) • f x✝
case h.e'_3.h.e_f.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ cexp (↑x✝¹.log * ↑x✝ * I) = cexp (-(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))) * I)) ∨ f x✝ = 0