Theorem: rectangleIntegral_symm (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 z w = RectangleIntegral f w z
Tactic:
simp_rw [RectangleIntegral, HIntegral, VIntegral, intervalIntegral.integral_symm w.re,
  intervalIntegral.integral_symm w.im, sub_neg_eq_add, smul_neg, sub_neg_eq_add, ← sub_eq_add_neg,
  neg_add_eq_sub, sub_add_eq_add_sub]
State after:
no goals