no goals
ι : Type ?u.7559135
𝕜 : Type ?u.7559138
E : Type u_1
F : Type ?u.7559144
A : Type ?u.7559147
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 [sub_neg_eq_add] using IntervalIntegrable.comp_add_right hf (-c)