Integral indicator tail even

lemma integral_indicator_tail_even {f : ℝ → ℝ} {R : ℝ} (hR : 0 < R)    (heven : ∀ x, f (-x) = f x)    (hint : IntegrableOn f (Set.Ici R)) :    ∫ z, Set.indicator {z : ℝ | R ≤ |z|} f z    = 2 * ∫ z in Set.Ici R, f z := by  -- Split {z | R ≤ |z|} into two parts: (-∞, -R] ∪ [R, ∞)  have h_split : {z : ℝ | R ≤ |z|} = Set.Iic (-R) ∪ Set.Ici R := by    ext z    simp only [Set.mem_setOf, Set.mem_union, Set.mem_Iic, Set.mem_Ici]    constructor    · intro h      by_cases hz : z < 0      · left        simp [abs_of_neg hz] at h        linarith      · right        push_neg at hz        simp [abs_of_nonneg hz] at h        exact h    · intro h      cases h with      | inl h => simp [abs_of_nonpos (by linarith : z ≤ 0)]; linarith      | inr h => simp [abs_of_nonneg (by linarith : 0 ≤ z)]; exact h   have h_disj : Disjoint (Set.Iic (-R)) (Set.Ici R) := by    rw [Set.disjoint_iff]    intro z hz    simp only [Set.mem_inter_iff, Set.mem_Iic, Set.mem_Ici] at hz    obtain ⟨h1, h2⟩ := hz    linarith   rw [h_split, Set.indicator_union_of_disjoint h_disj]   rw [integral_add]  swap; · -- integrability on Iic (-R)    have h_int_left : IntegrableOn f (Set.Iic (-R)) := by      rw [← Measure.map_neg_eq_self (volume : Measure ℝ)]      let m : MeasurableEmbedding (fun x : ℝ => -x) := (Homeomorph.neg ℝ).measurableEmbedding      rw [m.integrableOn_map_iff]      simp_rw [Function.comp_def, Set.neg_preimage, Set.neg_Iic, neg_neg]      convert hint using 2      aesop    rw [integrable_indicator_iff measurableSet_Iic]    exact h_int_left   swap; ·    rw [integrable_indicator_iff measurableSet_Ici]    exact hint   have h_left_eq_right :      ∫ z, Set.indicator (Set.Iic (-R)) f z = ∫ z, Set.indicator (Set.Ici R) f z := by    rw [integral_indicator measurableSet_Iic]    rw [integral_indicator measurableSet_Ici]    -- Strategy: show ∫_{Iic(-R)} f = ∫_{Ici R} f using negation and evenness    have : ∫ x in Set.Iic (-R), f x = ∫ x in Set.Ici R, f (-x) := by      calc ∫ x in Set.Iic (-R), f x          = ∫ x in Set.Ioi R, f (-x) := by              convert integral_comp_neg_Iic (c := -R) f using 2              aesop              aesop              aesop        _ = ∫ x in Set.Ici R, f (-x) := by              rw [← integral_Ici_eq_integral_Ioi']              aesop    rw [this]    apply setIntegral_congr_ae measurableSet_Ici    filter_upwards with z hz    exact heven z  rw [h_left_eq_right, integral_indicator measurableSet_Ici, ← two_mul]