field_simp
case h.e'_3.h.e_f.h.h.e_z.e_a
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✝ : ℝ
⊢ x✝¹.log * x✝ = -(2 * π * (x✝ * (-x✝¹.log / (2 * π))))
case h.e'_3.h.e_f.h.h.e_z.e_a
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✝ : ℝ
⊢ x✝¹.log * x✝ = x✝ * x✝¹.log