refine verticalIntegral_eq_verticalIntegral ((isHolomorphicOn xpos).mono ?_)
  (tendsto_zero_Lower xpos σ' σ'') (tendsto_zero_Upper xpos σ' σ'')
  (isIntegrable xpos (fun h ↦ hσ0 (h ▸ left_mem_uIcc)) (fun h ↦ hσ1 (h ▸ left_mem_uIcc)))
  (isIntegrable xpos (fun h ↦ hσ0 (h ▸ right_mem_uIcc)) (fun h ↦ hσ1 (h ▸ right_mem_uIcc)))
x σ σ'✝ σ''✝ T σ' σ'' : ℝ
xpos : 0 < x
hσ0 : 0 ∉ [[σ', σ'']]
hσ1 : -1 ∉ [[σ', σ'']]
⊢ VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
x σ σ'✝ σ''✝ T σ' σ'' : ℝ
xpos : 0 < x
hσ0 : 0 ∉ [[σ', σ'']]
hσ1 : -1 ∉ [[σ', σ'']]
⊢ [[σ', σ'']] ×ℂ univ ⊆ {0, -1}ᶜ