no goals
ι : Type ?u.14946556
𝕜 : Type ?u.14946559
E : Type u_1
F : Type ?u.14946565
A : Type ?u.14946568
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d✝ : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ (∫ (x : ℝ) in a..b, f (d - x / c)) = c • ∫ (x : ℝ) in d - b / c..d - a / c, f x
simpa only [div_eq_inv_mul, inv_inv] using integral_comp_sub_mul f (inv_ne_zero hc) d