congr <;> ext <;> congr 1 <;> simp [Complex.ext_iff]
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 : ℂ → E
z w p : ℂ
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I - p)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I - p)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I - p)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I - p) =
    (((∫ (x : ℝ) in z.re..w.re, f (↑(x - p.re) + ↑(z.im - p.im) * I)) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(x - p.re) + ↑(w.im - p.im) * I)) +
        I • ∫ (x : ℝ) in z.im..w.im, f (↑(w.re - p.re) + ↑(x - p.im) * I)) -
      I • ∫ (x : ℝ) in z.im..w.im, f (↑(z.re - p.re) + ↑(x - p.im) * I)
no goals