congr
case h.e'_3.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✝ : ℝ
⊢ ∫ (t : ℝ), f t * cexp (↑x✝.log * ↑t * I) = 𝓕 f (-x✝.log / (2 * π))
case h.e'_3.h.e_f
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✝ : ℝ
⊢ (fun t => f t * cexp (↑x✝.log * ↑t * I)) = fun v => 𝐞 (-((innerₗ ℝ) v) (-x✝.log / (2 * π))) • f v