E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x => -x
⊢ (∫ (x : ℝ) in Iic c, f (-x)) = ∫ (x : ℝ) in Ioi (-c), f x
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
c : ℝ
f : ℝ → E
⊢ (∫ (x : ℝ) in Iic c, f (-x)) = ∫ (x : ℝ) in Ioi (-c), f x
have A : MeasurableEmbedding fun x : ℝ => -x :=
  (Homeomorph.neg ℝ).closedEmbedding.measurableEmbedding
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x => -x
this : (∫ (y : ℝ) in Ici (-c), f y ∂Measure.map (fun x => -x) volume) = ∫ (x : ℝ) in (fun x => -x) ⁻¹' Ici (-c), f (-x)
⊢ (∫ (x : ℝ) in Iic c, f (-x)) = ∫ (x : ℝ) in Ioi (-c), f x
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x => -x
⊢ (∫ (x : ℝ) in Iic c, f (-x)) = ∫ (x : ℝ) in Ioi (-c), f x
have := @MeasurableEmbedding.set_integral_map _ _ _ _ volume _ _ _ _ _  A f (Ici (-c))
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x => -x
this : (∫ (y : ℝ) in Ici (-c), f y) = ∫ (x : ℝ) in (fun x => -x) ⁻¹' Ici (-c), f (-x)
⊢ (∫ (x : ℝ) in Iic c, f (-x)) = ∫ (x : ℝ) in Ioi (-c), f x
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x => -x
this : (∫ (y : ℝ) in Ici (-c), f y ∂Measure.map (fun x => -x) volume) = ∫ (x : ℝ) in (fun x => -x) ⁻¹' Ici (-c), f (-x)
⊢ (∫ (x : ℝ) in Iic c, f (-x)) = ∫ (x : ℝ) in Ioi (-c), f x
rw [Measure.map_neg_eq_self (volume : Measure ℝ)] at this
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x => -x
this : (∫ (y : ℝ) in Ici (-c), f y) = ∫ (x : ℝ) in (fun x => -x) ⁻¹' Ici (-c), f (-x)
⊢ (∫ (x : ℝ) in Iic c, f (-x)) = ∫ (x : ℝ) in Ioi (-c), f x
simp_rw [← integral_Ici_eq_integral_Ioi, this, neg_preimage, preimage_neg_Ici, neg_neg]