ResidueTheoremOnRectangleWithSimplePole

@[blueprint  (title := "ResidueTheoremOnRectangleWithSimplePole")  (statement := /--  Suppose that $f$ is a holomorphic function on a rectangle,  except for a simple pole at $p$.  By the latter, we mean that there is a function $g$  holomorphic on the rectangle such that,  $f = g + A/(s-p)$ for some $A\in\C$. Then the integral of  $f$ over the rectangle is $A$.  -/)  (proof := /--  Replace $f$ with $g + A/(s-p)$ in the integral.  The integral of $g$ vanishes by  Lemma \ref{HolomorphicOn.vanishesOnRectangle}.  To evaluate the integral of $1/(s-p)$, pull everything to a  square about the origin using  Lemma \ref{RectanglePullToNhdOfPole}, and rescale by $c$;  what remains is handled by  Lemma \ref{ResidueTheoremAtOrigin}.  -/)  (latexEnv := "lemma")]lemma ResidueTheoremOnRectangleWithSimplePole {f g : ℂ → ℂ} {z w p A : ℂ}    (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im)    (pInRectInterior : Rectangle z w ∈ 𝓝 p) (gHolo : HolomorphicOn g (Rectangle z w))    (principalPart : Set.EqOn (f - fun s ↦ A / (s - p)) g (Rectangle z w \ {p})) :    RectangleIntegral' f z w = A := by  have principalPart' : Set.EqOn f (g + (fun s ↦ A / (s - p))) (Rectangle z w \ {p}) :=    fun s hs => by rw [Pi.add_apply, ← principalPart hs, Pi.sub_apply, sub_add_cancel]  have : Set.EqOn f (g + (fun s ↦ A / (s - p))) (RectangleBorder z w) :=    principalPart'.mono <| Set.subset_sdiff.mpr      ⟨rectangleBorder_subset_rectangle z w,        disjoint_singleton_right.mpr          (not_mem_rectangleBorder_of_rectangle_mem_nhds pInRectInterior)⟩  rw [RectangleIntegral'_congr this]  have t1 : RectangleBorderIntegrable g z w :=    gHolo.rectangleBorderIntegrable  have t2 : HolomorphicOn (fun s ↦ A / (s - p)) (Rectangle z w \ {p}) := by    apply DifferentiableOn.mono (t := {p}ᶜ)    · apply DifferentiableOn.div      · exact differentiableOn_const _      · exact DifferentiableOn.sub differentiableOn_id (differentiableOn_const _)      · exact fun x hx => by          rw [sub_ne_zero]          exact hx    · rintro s ⟨_, hs⟩      exact hs  have t3 : RectangleBorderIntegrable (fun s ↦ A / (s - p)) z w :=    HolomorphicOn.rectangleBorderIntegrable' t2 pInRectInterior  rw [RectangleIntegral', RectangleBorderIntegrable.add t1 t3, smul_add]  rw [gHolo.vanishesOnRectangle (by rfl), smul_zero, zero_add]  exact ResidueTheoremInRectangle zRe_le_wRe zIm_le_wIm pInRectInterior