rectangle_argumentChange_eq_two_pi_sum_meromorphicOrderAt

theorem rectangle_argumentChange_eq_two_pi_sum_meromorphicOrderAt    {f : ℂ → ℂ} {z w : ℂ} {argumentChange : ℝ}    (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im)    (hf : MeromorphicOn f (Rectangle z w))    (hlog : MeromorphicOn (logDeriv f) (Rectangle z w))    (hfinite_order : ∀ p ∈ Rectangle z w, meromorphicOrderAt f p ≠ ⊤)    (hno_boundary :      Disjoint (RectangleBorder z w) (MeromorphicOn.divisor f (Rectangle z w)).support)    (hargumentChange :      (argumentChange : ℂ) =        (2 * Real.pi : ℂ) * RectangleIntegral' (logDeriv f) z w) :    argumentChange =      2 * Real.pi *        ∑ p ∈ (divisor_support_rectangle_finite f z w).toFinset,          (((MeromorphicOn.divisor f (Rectangle z w)) p : ℤ) : ℝ) := by  classical  have hcomplex :      (argumentChange : ℂ) =        (2 * Real.pi : ℂ) *          ∑ p ∈ (divisor_support_rectangle_finite f z w).toFinset,            (((MeromorphicOn.divisor f (Rectangle z w)) p : ℤ) : ℂ) := by    rw [hargumentChange]    rw [rectangleIntegral_logDeriv_eq_sum_meromorphicOrderAt zRe_le_wRe zIm_le_wIm      hf hlog hfinite_order hno_boundary]  have hre := congrArg Complex.re hcomplex  simpa [Finset.mul_sum, mul_assoc] using hre