simp
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ (f n * (↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I))) • ψ y = (f n / ↑n ^ (↑σ' + ↑y * I)) • (ψ y * ↑x ^ (↑y * I))
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n * (↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)) * ψ y = f n / ↑n ^ (↑σ' + ↑y * I) * (ψ y * ↑x ^ (↑y * I))