Theorem: rectangleIntegral_symm_re (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 : ℂ → E
z w : ℂ
⊢ RectangleIntegral f (↑w.re + ↑z.im * I) (↑z.re + ↑w.im * I) = -RectangleIntegral f z w
Tactic:
simp [RectangleIntegral, ← sub_eq_zero]
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 : ℂ → E
z w : ℂ
⊢ HIntegral f w.re z.re z.im - HIntegral f w.re z.re w.im + VIntegral f z.re z.im w.im - VIntegral f w.re z.im w.im -
        (VIntegral f z.re z.im w.im -
          (HIntegral f z.re w.re z.im - HIntegral f z.re w.re w.im + VIntegral f w.re z.im w.im)) -
      0 =
    0

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 : ℂ → E
z w : ℂ
⊢ HIntegral f w.re z.re z.im - HIntegral f w.re z.re w.im + VIntegral f z.re z.im w.im - VIntegral f w.re z.im w.im -
        (VIntegral f z.re z.im w.im -
          (HIntegral f z.re w.re z.im - HIntegral f z.re w.re w.im + VIntegral f w.re z.im w.im)) -
      0 =
    0
Tactic:
rw [HIntegral_symm (y := z.im), HIntegral_symm (y := w.im)]
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 : ℂ → E
z w : ℂ
⊢ -HIntegral f z.re w.re z.im - -HIntegral f z.re w.re w.im + VIntegral f z.re z.im w.im - VIntegral f w.re z.im w.im -
        (VIntegral f z.re z.im w.im -
          (HIntegral f z.re w.re z.im - HIntegral f z.re w.re w.im + VIntegral f w.re z.im w.im)) -
      0 =
    0

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 : ℂ → E
z w : ℂ
⊢ -HIntegral f z.re w.re z.im - -HIntegral f z.re w.re w.im + VIntegral f z.re z.im w.im - VIntegral f w.re z.im w.im -
        (VIntegral f z.re z.im w.im -
          (HIntegral f z.re w.re z.im - HIntegral f z.re w.re w.im + VIntegral f w.re z.im w.im)) -
      0 =
    0
Tactic:
abel
State after:
no goals