calc
  _ =  ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * deriv (@g s) x := ?_
  _ = -∫ (x : ℝ) in Ioi 0, deriv (fun x ↦ ↑(Ψ x)) x * @g s x := ?_
  _ = -∫ (x : ℝ) in Ioi 0, deriv Ψ x * @g s x := ?_
  _ = -∫ (x : ℝ) in Ioi 0, deriv Ψ x * x ^ s / s := by simp only [mul_div, g]
  _ = _ := ?_
𝕂 : 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
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * ↑x ^ (s - 1) = -(1 / s) * ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s
case calc_1
𝕂 : 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
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * ↑x ^ (s - 1) = ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * deriv g x

case calc_2
𝕂 : 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
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv (fun x => ↑(Ψ x)) x * g x

case calc_3
𝕂 : 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
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ -∫ (x : ℝ) in Ioi 0, deriv (fun x => ↑(Ψ x)) x * g x = -∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * g x

case calc_4
𝕂 : 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
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ -∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s / s = -(1 / s) * ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s