no goals
ι : Type ?u.7443118
𝕜 : Type ?u.7443121
E : Type u_1
F : Type ?u.7443127
A : Type ?u.7443130
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
⊢ IntervalIntegrable (fun x => f (c + x)) volume (a - c) (b - c)
simpa only [add_comm] using IntervalIntegrable.comp_add_right hf c