rw [← Complex.cpow_mul _ ?_ ?_, mul_sub]
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * ↑ε⁻¹ * ↑x ^ (s - 1) =
    1 / ↑ε * ↑x ^ ↑(1 / ε - 1) * (↑(Ψ (x ^ (1 / ε))) * (↑x ^ (1 / ↑ε)) ^ (↑ε * s - 1))
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ↑(Ψ (x ^ (1 / ε))) * ↑ε⁻¹ * ↑x ^ (s - 1) =
    1 / ↑ε * ↑x ^ ↑(1 / ε - 1) * (↑(Ψ (x ^ (1 / ε))) * ↑x ^ (1 / ↑ε * (↑ε * s) - 1 / ↑ε * 1))

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ -π < ((↑x).log * (1 / ↑ε)).im

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ ((↑x).log * (1 / ↑ε)).im ≤ π