no goals
ι : Type ?u.7203111
𝕜 : Type ?u.7203114
E : Type u_1
F : Type ?u.7203120
A : Type ?u.7203123
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
⊢ IntervalIntegrable (fun x => f (x * c)) volume (a / c) (b / c)
simpa only [mul_comm] using comp_mul_left hf c