Theorem: RectangleBorderIntegrable.add (PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean)

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
⊢ RectangleIntegral (f + g) z w = RectangleIntegral f z w + RectangleIntegral g z w
Tactic:
dsimp [RectangleIntegral, HIntegral, VIntegral]
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
⊢ (((∫ (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))

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
⊢ (((∫ (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.1 hg.1
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)
⊢ (((∫ (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))

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)
⊢ (((∫ (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.1 hg.2.1
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)
⊢ (((∫ (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))

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)
⊢ (((∫ (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.1 hg.2.2.1
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)
⊢ (((∫ (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))

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
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))

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)
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))
Tactic:
additive_combination h₁ - h₂ + I • h₃ - I • h₄
State after:
no goals