rw [RectangleIntegral.translate', RectangleIntegral']
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
⊢ RectangleIntegral' (fun s => c / (s - p)) z w = c
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : (z.re < p.re ∧ p.re < w.re) ∧ z.im < p.im ∧ p.im < w.im
⊢ (1 / (2 * ↑π * I)) • RectangleIntegral (HDiv.hDiv c) (z - p) (w - p) = c