have := (intervalIntegral_tendsto_integral_Iic (-T) int.restrict tendsto_id).const_smul I
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 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 y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
s : ℝ
int : Integrable (fun y => f (↑s + ↑y * I)) volume
⊢ Tendsto (fun U => I * ∫ (y : ℝ) in -U..-T, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Iic (-T), f (↑s + ↑y * I)))
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 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 y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
s : ℝ
int : Integrable (fun y => f (↑s + ↑y * I)) volume
this :
  Tendsto (fun x => I • ∫ (x : ℝ) in id x..-T, f (↑s + ↑x * I)) atBot
    (𝓝 (I • ∫ (x : ℝ) in Iic (-T), f (↑s + ↑x * I) ∂volume))
⊢ Tendsto (fun U => I * ∫ (y : ℝ) in -U..-T, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Iic (-T), f (↑s + ↑y * I)))