no goals
ι : Type ?u.7085574
𝕜 : Type ?u.7085577
E : Type u_1
F : Type ?u.7085583
A : Type ?u.7085586
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
c : ℝ
hc : c ≠ 0
h : IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)
⊢ IntervalIntegrable f volume a b
simpa [hc] using h.comp_mul_left c⁻¹