convert (hbot.comp tendsto_neg_atTop_atBot) using 1
σ σ' 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
⊢ Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
case h.e'_3
σ σ' 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
⊢ (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) = (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) ∘ Neg.neg