rw [HIntegral_symm (y := z.im), HIntegral_symm (y := w.im)]
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 : ℂ
⊢ HIntegral f w.re z.re z.im - HIntegral f w.re z.re w.im + VIntegral f z.re z.im w.im - VIntegral f w.re z.im w.im -
        (VIntegral f z.re z.im w.im -
          (HIntegral f z.re w.re z.im - HIntegral f z.re w.re w.im + VIntegral f w.re z.im w.im)) -
      0 =
    0
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 : ℂ
⊢ -HIntegral f z.re w.re z.im - -HIntegral f z.re w.re w.im + VIntegral f z.re z.im w.im - VIntegral f w.re z.im w.im -
        (VIntegral f z.re z.im w.im -
          (HIntegral f z.re w.re z.im - HIntegral f z.re w.re w.im + VIntegral f w.re z.im w.im)) -
      0 =
    0