rfl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z✝ w✝ p✝ c A✝ : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
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 : EqOn (f - fun s => A / (s - p)) g (Rectangle z w \ {p})
principalPart' : EqOn f (g + fun s => A / (s - p)) (Rectangle z w \ {p})
this : EqOn f (g + fun s => A / (s - p)) (RectangleBorder z w)
t1 : RectangleBorderIntegrable g z w
t2 : HolomorphicOn (fun s => A / (s - p)) (Rectangle z w \ {p})
t3 : RectangleBorderIntegrable (fun s => A / (s - p)) z w
⊢ Rectangle z w ⊆ Rectangle z w
no goals