linarith
σ σ' : ℝ
f : ℂ → ℂ
p : ℂ
hσ : σ < p.re ∧ p.re < σ'
hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p})
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
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
this✝² : Icc σ σ' ×ℂ univ ∈ 𝓝 p
c' : ℝ
hc'0 : 0 < c'
hc' : Square p c' ⊆ Icc σ σ' ×ℂ univ
c : ℝ
hc0 : 0 < c
hcc' : c < c'
hsub : Square p c ⊆ Icc σ σ' ×ℂ univ
y : ℝ
hy : y ∈ Ioi ((c - p.im) ⊔ (c + p.im))
this✝¹ : c - p.im < y ∧ c + p.im < y
this✝ : c + σ ≤ p.re
this : c + p.re ≤ σ'
⊢ 0 ≤ y
no goals