no goals
ι : Type ?u.14957297
𝕜 : Type ?u.14957300
E : Type u_1
F : Type ?u.14957306
A : Type ?u.14957309
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d✝ : ℝ
f : ℝ → E
d : ℝ
⊢ (∫ (x : ℝ) in a..b, f (x - d)) = ∫ (x : ℝ) in a - d..b - d, f x
simpa only [sub_eq_add_neg] using integral_comp_add_right f (-d)