CH2.RectangleIntegral_tendsTo_UpperU'

lemma RectangleIntegral_tendsTo_UpperU' {σ σ' T : ℝ} {f : ℂ → ℂ}    (htop : Filter.Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + y * I)) Filter.atTop (nhds 0))    (hleft : IntegrableOn (fun (y : ℝ) ↦ f (σ + y * I)) (Set.Ici T))    (hright : IntegrableOn (fun (y : ℝ) ↦ f (σ' + y * I)) (Set.Ici T)) :    Filter.Tendsto (fun (U : ℝ) ↦ RectangleIntegral f (σ + I * T) (σ' + I * U)) Filter.atTop      (nhds (UpperUIntegral f σ σ' T)) := by  have h_re  (s : ℝ) (t : ℝ) : (s  + I * t).re = s  := by simp  have h_im  (s : ℝ) (t : ℝ) : (s  + I * t).im = t  := by simp  have hbot : Filter.Tendsto (fun (_ : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + T * I)) Filter.atTop      (nhds <| ∫ (x : ℝ) in σ..σ', f (x + T * I)) := tendsto_const_nhds  have hvert (s : ℝ) (int : IntegrableOn (fun (y : ℝ) ↦ f (s + y * I)) (Set.Ici T)) :      Filter.Tendsto (fun (U : ℝ) ↦ I * ∫ (y : ℝ) in T..U, f (s + y * I)) Filter.atTop        (nhds <| I * ∫ (y : ℝ) in Set.Ioi T, f (s + y * I)) := by    refine (intervalIntegral_tendsto_integral_Ioi T ?_ Filter.tendsto_id).const_smul I    exact int.mono_set (Set.Ioi_subset_Ici le_rfl)  have := ((hbot.sub htop).add (hvert σ' hright)).sub (hvert σ hleft)  simpa only [RectangleIntegral, UpperUIntegral, h_re, h_im, sub_zero,    ← integral_Ici_eq_integral_Ioi]