filter_upwards [eventually_ge_atTop T]
case hf
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
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
⊢ (fun U => RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑U)) =ᶠ[atTop] fun x => 0
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
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
⊢ ∀ (a : ℝ), T ≤ a → RectangleIntegral f (↑σ + I * ↑T) (↑σ' + I * ↑a) = 0