ι : Type ?u.14923117
𝕜 : Type ?u.14923120
E : Type u_1
F : Type ?u.14923126
A : Type ?u.14923129
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 + -c * x)) = c⁻¹ • ∫ (x : ℝ) in d + -c * b..d + -c * a, f x
ι : Type ?u.14923117
𝕜 : Type ?u.14923120
E : Type u_1
F : Type ?u.14923126
A : Type ?u.14923129
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 - c * x)) = c⁻¹ • ∫ (x : ℝ) in d - c * b..d - c * a, f x
simp only [sub_eq_add_neg, neg_mul_eq_neg_mul]
ι : Type ?u.14923117
𝕜 : Type ?u.14923120
E : Type u_1
F : Type ?u.14923126
A : Type ?u.14923129
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d✝ : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ((-c)⁻¹ • -∫ (x : ℝ) in d + -c * b..d + -c * a, f x) = c⁻¹ • ∫ (x : ℝ) in d + -c * b..d + -c * a, f x
ι : Type ?u.14923117
𝕜 : Type ?u.14923120
E : Type u_1
F : Type ?u.14923126
A : Type ?u.14923129
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 + -c * x)) = c⁻¹ • ∫ (x : ℝ) in d + -c * b..d + -c * a, f x
rw [integral_comp_add_mul f (neg_ne_zero.mpr hc) d, integral_symm]
no goals
ι : Type ?u.14923117
𝕜 : Type ?u.14923120
E : Type u_1
F : Type ?u.14923126
A : Type ?u.14923129
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d✝ : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ((-c)⁻¹ • -∫ (x : ℝ) in d + -c * b..d + -c * a, f x) = c⁻¹ • ∫ (x : ℝ) in d + -c * b..d + -c * a, f x
simp only [inv_neg, smul_neg, neg_neg, neg_smul]