no goals
ι : Type ?u.14958229
𝕜 : Type ?u.14958232
E : Type u_1
F : Type ?u.14958238
A : Type ?u.14958241
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d✝ : ℝ
f : ℝ → E
d : ℝ
⊢ (∫ (x : ℝ) in a..b, f (d - x)) = ∫ (x : ℝ) in d - b..d - a, f x
simpa only [one_mul, one_smul, inv_one] using integral_comp_sub_mul f one_ne_zero d