verticalIntegral_sub_verticalIntegral_eq_squareIntegral

lemma verticalIntegral_sub_verticalIntegral_eq_squareIntegral    {σ σ' : ℝ} {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)))    (hright : Integrable (fun (y : ℝ) ↦ f (σ' + y * I))) :    ∀ᶠ (c : ℝ) in 𝓝[>] 0, VerticalIntegral f σ' - VerticalIntegral f σ =    RectangleIntegral f (-c - c * I + p) (c + c * I + p) := by  have : Icc σ σ' ×ℂ univ ∈ 𝓝 p := by    rw [← mem_interior_iff_mem_nhds, Complex.interior_reProdIm, interior_Icc, interior_univ]    refine ⟨⟨?_, ?_⟩, trivial⟩ <;> linarith  obtain ⟨c', hc'0, hc'⟩ := ((nhds_hasBasis_square p).1 _).mp this  filter_upwards [Ioo_mem_nhdsGT hc'0] with c ⟨hc0, hcc'⟩  have hsub : Square p c ⊆ Icc σ σ' ×ℂ univ := (square_subset_square hc0 hcc'.le).trans hc'  apply tendsto_nhds_unique (RectangleIntegral_tendsTo_VerticalIntegral hbot htop hleft hright)  apply Filter.EventuallyEq.tendsto  filter_upwards [Filter.Ioi_mem_atTop ((c - p.im) ⊔ (c + p.im))] with y hy  have : c - p.im < y ∧ c + p.im < y := sup_lt_iff.mp hy  have : c + σ ≤ p.re := by simpa using (hsub ⟨left_mem_uIcc, left_mem_uIcc⟩).1.1  have : c + p.re ≤ σ' := by simpa using (hsub ⟨right_mem_uIcc, right_mem_uIcc⟩).1.2  apply RectanglePullToNhdOfPole'  · simpa using ⟨by linarith, by linarith, by linarith⟩  · exact square_mem_nhds p (ne_of_gt hc0)  · apply RectSubRect' <;> simpa using by linarith  · refine hf.mono (Set.sdiff_subset_sdiff ?_ subset_rfl)    simpa [Rectangle, uIcc_of_lt (hσ.1.trans hσ.2)] using! fun x ⟨hx, _⟩ ↦ ⟨hx, trivial⟩