Theorem: Perron.contourPull (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
x σ σ'✝ σ''✝ T σ' σ'' : ℝ
xpos : 0 < x
hσ0 : 0 ∉ [[σ', σ'']]
hσ1 : -1 ∉ [[σ', σ'']]
⊢ VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
Tactic:
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)))
State after:
x σ σ'✝ σ''✝ T σ' σ'' : ℝ
xpos : 0 < x
hσ0 : 0 ∉ [[σ', σ'']]
hσ1 : -1 ∉ [[σ', σ'']]
⊢ [[σ', σ'']] ×ℂ univ ⊆ {0, -1}ᶜ

State before:
x σ σ'✝ σ''✝ T σ' σ'' : ℝ
xpos : 0 < x
hσ0 : 0 ∉ [[σ', σ'']]
hσ1 : -1 ∉ [[σ', σ'']]
⊢ [[σ', σ'']] ×ℂ univ ⊆ {0, -1}ᶜ
Tactic:
rintro ⟨x, y⟩ ⟨hx, hy⟩ ⟨hc | hc⟩ <;> simp_all [Complex.ext_iff]
State after:
no goals