rw [← integral_comp_rpow_Ioi (fun z ↦ ((Ψ z) : ℂ) * (z : ℂ) ^ ((ε : ℂ) * s - 1))
  (one_div_ne_zero (ne_of_gt εpos))]
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ ∫ (x : ℝ) in Ioi 0, (fun x => ↑(Ψ (x ^ (1 / ε)) / ε)) x * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, (fun x => ↑(Ψ x)) x * ↑x ^ (↑ε * s - 1)
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ ∫ (x : ℝ) in Ioi 0, (fun x => ↑(Ψ (x ^ (1 / ε)) / ε)) x * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))