abel
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 σ σ' (-T) - HIntegral f σ σ' T + VIntegral f σ' (-T) T - VIntegral f σ (-T) 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))
no goals