rw [Complex.cpow_def_of_ne_zero (ofReal_ne_zero.mpr hx), ofReal_log hx']
case h
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
x : ℝ
hx : x ≠ 0
hx' : 0 ≤ x
t : ℝ
⊢ ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
case h
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
x : ℝ
hx : x ≠ 0
hx' : 0 ≤ x
t : ℝ
⊢ cexp ((↑x).log * (↑t * I)) = cexp ((↑x).log * ↑t * I)