rw [Complex.ofReal_log hx.le]
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ -(↑y * ((↑n).log - ↑x.log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ -(↑y * ((↑n).log - (↑x).log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)