have hvert (s : ℝ) (int : Integrable (fun (y : ℝ) ↦ f (s + y * I))) :
    Tendsto (fun (U : ℝ) ↦ I * ∫ (y : ℝ) in T..U, f (s + y * I)) atTop (𝓝 <| I * ∫ (y : ℝ) in Ioi T, f (s + y * I)) := by
  exact (intervalIntegral_tendsto_integral_Ioi T int.restrict tendsto_id).const_smul I
σ σ' T : ℝ
f : ℂ → ℂ
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s + I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s + I * ↑t).im = t
hbot : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)))
⊢ Tendsto (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) atTop (𝓝 (UpperUIntegral f σ σ' T))
σ σ' T : ℝ
f : ℂ → ℂ
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s + I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s + I * ↑t).im = t
hbot : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x + ↑T * I)))
hvert :
  ∀ (s : ℝ),
    Integrable (fun y => f (↑s + ↑y * I)) volume →
      Tendsto (fun U => I * ∫ (y : ℝ) in T..U, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Ioi T, f (↑s + ↑y * I)))
⊢ Tendsto (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) atTop (𝓝 (UpperUIntegral f σ σ' T))