rw [integral_const_div_re_add_self h1.ne, integral_const_div_re_add_self h3.ne.symm]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z✝ w✝ p c✝ A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
⊢ (((∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑w.im * I)) +
        I * ∫ (y : ℝ) in z.im..w.im, c / (↑w.re + ↑y * I)) -
      I * ∫ (y : ℝ) in z.im..w.im, c / (↑z.re + ↑y * I) =
    2 * I * ↑π * 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₂ σ : ℝ
z w c : ℂ
h1 : z.re < 0
h2 : z.im < 0
h3 : 0 < w.re
h4 : 0 < w.im
⊢ ((∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, c / (↑x + ↑w.im * I)) +
        I *
          (c / I * (↑(w.im ^ 2 + (-w.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-w.re) ^ 2).log / 2) -
            c / I * I * (↑(w.im / -w.re).arctan - ↑(z.im / -w.re).arctan)) -
      I *
        (c / I * (↑(w.im ^ 2 + (-z.re) ^ 2).log / 2 - ↑(z.im ^ 2 + (-z.re) ^ 2).log / 2) -
          c / I * I * (↑(w.im / -z.re).arctan - ↑(z.im / -z.re).arctan)) =
    2 * I * ↑π * c