no goals
ι : Type ?u.7793606
𝕜 : Type ?u.7793609
E : Type u_1
F : Type ?u.7793615
A : Type ?u.7793618
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 (c - a) (c - b)
simpa only [neg_sub, ← sub_eq_add_neg] using iff_comp_neg.mp (hf.comp_add_left c)