simp [hx]
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)
x✝ : ℝ
hx : ∀ (t : ℝ), ↑x✝ ^ (↑t * I) = cexp (↑x✝.log * ↑t * I)
x : ℝ
⊢ (fun t => f t * ↑x✝ ^ (↑t * I)) x = (fun t => f t * cexp (↑x✝.log * ↑t * I)) x
no goals