let g {s : ℂ} := fun (x : ℝ)  ↦ x ^ s / s
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
⊢ ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * ↑x ^ (s - 1) = -(1 / s) * ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
⊢ ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * ↑x ^ (s - 1) = -(1 / s) * ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s