E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
c : ℝ
f : ℝ → E
⊢ (∫ (x : ℝ) in Iic (-c), f (- -x)) = ∫ (x : ℝ) in Iic (- - -c), f x
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
c : ℝ
f : ℝ → E
⊢ (∫ (x : ℝ) in Ioi c, f (-x)) = ∫ (x : ℝ) in Iic (-c), f x
rw [← neg_neg c, ← integral_comp_neg_Iic]
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
c : ℝ
f : ℝ → E
⊢ (∫ (x : ℝ) in Iic (-c), f (- -x)) = ∫ (x : ℝ) in Iic (- - -c), f x
simp only [neg_neg]