rw [one_div_mul_cancel (by exact slitPlane_ne_zero (Or.inl εpos)), mul_comm (1 / (ε:ℂ)),
    mul_comm, ← mul_assoc, ← mul_assoc]
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
log_x_real : (↑x).log.im = 0
⊢ 1 / ↑ε * ↑x ^ (1 / ↑ε - 1) * ↑(Ψ (x ^ (1 / ε))) * ↑x ^ (1 / ↑ε * ↑ε * s - 1 / ↑ε) =
    ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (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 * s - 1 / ↑ε) * ↑x ^ (1 / ↑ε - 1) * (1 / ↑ε) * ↑(Ψ (x ^ (1 / ε))) = ↑(Ψ (x ^ (1 / ε))) * (↑ε)⁻¹ * ↑x ^ (s - 1)