no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
⊢ IntegrableOn (fun x => x ^ (p - 1) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
simpa only [← integrableOn_Ioi_comp_rpow_iff f hp, mul_smul] using
  (integrable_smul_iff (abs_pos.mpr hp).ne' _).symm