no goals
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ IntegrableOn (fun x => f (x * a)) (Ioi c) ↔ IntegrableOn f (Ioi (c * a))
simpa only [mul_comm, MulZeroClass.mul_zero] using integrableOn_Ioi_comp_mul_left_iff f c ha