have := integral_comp_rpow_Ioi (fun y ↦ f y / y) (p := -1) (by simp)
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
⊢ ∫ (y : ℝ) in Ioi 0, f (1 / y) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
⊢ ∫ (y : ℝ) in Ioi 0, f (1 / y) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y