have l1 : ∀ᶠ x : ℝ in atTop, ∀ t : ℝ, x ^ (t * I) = exp (log x * t * I) := by
  filter_upwards [eventually_ne_atTop 0, eventually_ge_atTop 0] with x hx hx' t
  rw [Complex.cpow_def_of_ne_zero (ofReal_ne_zero.mpr hx), ofReal_log hx'] ; ring_nf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
⊢ Tendsto (fun x => ∫ (t : ℝ), f t * ↑x ^ (↑t * I)) atTop (𝓝 0)
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)
⊢ Tendsto (fun x => ∫ (t : ℝ), f t * ↑x ^ (↑t * I)) atTop (𝓝 0)