simp only [sub_re, mul_re, I_re, add_re, ofReal_re, I_im, ofReal_im, sub_im, mul_im, add_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₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      (HIntegral f (↑σ - I * ↑T).re (↑σ' + I * ↑T).re (↑σ - I * ↑T).im -
            HIntegral f (↑σ - I * ↑T).re (↑σ' + I * ↑T).re (↑σ' + I * ↑T).im +
          VIntegral f (↑σ' + I * ↑T).re (↑σ - I * ↑T).im (↑σ' + I * ↑T).im -
        VIntegral f (↑σ - I * ↑T).re (↑σ - I * ↑T).im (↑σ' + I * ↑T).im) =
    ((HIntegral f σ σ' T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) - I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      ((HIntegral f σ σ' (-T) - I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) +
        I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I))
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      (HIntegral f (σ - (0 * T - 1 * 0)) (σ' + (0 * T - 1 * 0)) (0 - (0 * 0 + 1 * T)) -
            HIntegral f (σ - (0 * T - 1 * 0)) (σ' + (0 * T - 1 * 0)) (0 + (0 * 0 + 1 * T)) +
          VIntegral f (σ' + (0 * T - 1 * 0)) (0 - (0 * 0 + 1 * T)) (0 + (0 * 0 + 1 * T)) -
        VIntegral f (σ - (0 * T - 1 * 0)) (0 - (0 * 0 + 1 * T)) (0 + (0 * 0 + 1 * T))) =
    ((HIntegral f σ σ' T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) - I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      ((HIntegral f σ σ' (-T) - I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) +
        I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I))