CH2.integral_Iic_one_eq_integral_Ioi_one_sub

theorem integral_Iic_one_eq_integral_Ioi_one_sub    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) :    (∫ r in Set.Iic (1 : ℝ), f r) = ∫ t in Set.Ioi (0 : ℝ), f (1 - t) := by  have hshift : (∫ x in Set.Iic (0 : ℝ), f (1 + x)) = ∫ x in Set.Iic (1 : ℝ), f x := by    have A : MeasurableEmbedding (fun x : ℝ => 1 + x) :=      (Homeomorph.addLeft (1 : ℝ)).measurableEmbedding    have h := MeasurableEmbedding.setIntegral_map (μ := volume) A f (Set.Iic (1 : ℝ))    rw [map_add_left_eq_self volume (1 : ℝ)] at h    have hpre : (fun x : ℝ => 1 + x) ⁻¹' Set.Iic (1 : ℝ) = Set.Iic (0 : ℝ) := by      ext x      simp [Set.mem_Iic]    rw [hpre] at h    exact h.symm  have hneg := integral_comp_neg_Iic (c := (0 : ℝ)) (f := fun t : ℝ => f (1 - t))  rw [neg_zero] at hneg  rw [← hneg]  rw [← hshift]  refine setIntegral_congr_fun (measurableSet_Iic : MeasurableSet (Set.Iic (0 : ℝ))) ?_  intro x hx  congr 1  ring