have h₁ := intervalIntegral.integral_add_adjacent_intervals f_int_x₀_a_bot f_int_a_x₁_bot
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ a x₀ x₁ y₀ y₁ : ℝ
f_int_x₀_a_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume x₀ a
f_int_a_x₁_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume a x₁
f_int_x₀_a_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume x₀ a
f_int_a_x₁_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume a x₁
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..a, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..a, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in y₀..y₁, f (↑a + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in a..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..y₁, f (↑a + ↑y * 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₂ σ a x₀ x₁ y₀ y₁ : ℝ
f_int_x₀_a_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume x₀ a
f_int_a_x₁_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume a x₁
f_int_x₀_a_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume x₀ a
f_int_a_x₁_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume a x₁
h₁ :
  (∫ (x : ℝ) in x₀..a, f (↑x + ↑y₀ * I)) + ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₀ * I) = ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..a, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..a, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in y₀..y₁, f (↑a + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in a..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..y₁, f (↑a + ↑y * I))