rwa [ResidueTheoremAtOrigin']
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
this : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
⊢ (1 / (2 * ↑π * I)) • RectangleIntegral (HDiv.hDiv c) (z - p) (w - p) = c
case h1
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
this : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
⊢ (z - p).re < 0

case h2
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
this : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
⊢ (z - p).im < 0

case h3
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
this : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
⊢ 0 < (w - p).re

case h4
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
this : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c
⊢ 0 < (w - p).im