Theorem: RectangleBorderIntegrable.add
Proof state before:
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 g : ℂ → E
hf : RectangleBorderIntegrable f z w
hg : RectangleBorderIntegrable g z w
h₁ :
  ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I) =
    (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) + ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)
h₂ :
  ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I) + g (↑x + ↑w.im * I) =
    (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) + ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑w.im * I)
h₃ :
  ∫ (x : ℝ) in z.im..w.im, f (↑w.re + ↑x * I) + g (↑w.re + ↑x * I) =
    (∫ (x : ℝ) in z.im..w.im, f (↑w.re + ↑x * I)) + ∫ (x : ℝ) in z.im..w.im, g (↑w.re + ↑x * I)
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I)) -
          ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I) + g (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) + g (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) + g (↑z.re + ↑y * I) =
    ((((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)) +
      ((((∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, g (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I))
Tactic:
have h₄ := intervalIntegral.integral_add hf.2.2.2 hg.2.2.2
Proof state after:
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 g : ℂ → E
hf : RectangleBorderIntegrable f z w
hg : RectangleBorderIntegrable g z w
h₁ :
  ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I) =
    (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) + ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)
h₂ :
  ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I) + g (↑x + ↑w.im * I) =
    (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) + ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑w.im * I)
h₃ :
  ∫ (x : ℝ) in z.im..w.im, f (↑w.re + ↑x * I) + g (↑w.re + ↑x * I) =
    (∫ (x : ℝ) in z.im..w.im, f (↑w.re + ↑x * I)) + ∫ (x : ℝ) in z.im..w.im, g (↑w.re + ↑x * I)
h₄ :
  ∫ (x : ℝ) in z.im..w.im, f (↑z.re + ↑x * I) + g (↑z.re + ↑x * I) =
    (∫ (x : ℝ) in z.im..w.im, f (↑z.re + ↑x * I)) + ∫ (x : ℝ) in z.im..w.im, g (↑z.re + ↑x * I)
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I)) -
          ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I) + g (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) + g (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) + g (↑z.re + ↑y * I) =
    ((((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)) +
      ((((∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, g (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I))