rectangleIntegral_logDeriv_eq_sum_meromorphicOrderAt

theorem rectangleIntegral_logDeriv_eq_sum_meromorphicOrderAt    {f : ℂ → ℂ} {z w : ℂ}    (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) :    RectangleIntegral' (logDeriv f) z w =      ∑ p ∈        ((divisor_support_rectangle_finite f z w).toFinset),          ((MeromorphicOn.divisor f (Rectangle z w)) p : ℂ) := by  classical  let R : Set ℂ := Rectangle z w  let D := MeromorphicOn.divisor f R  have hsupport : D.support.Finite := divisor_support_rectangle_finite f z w  have hlog_simple : HasSimplePolesOn (logDeriv f) R :=    logDeriv_hasSimplePolesOn_of_meromorphicOrderAt_ne_top hf hlog hfinite_order  have hlog_poles_eq :      R ∩ {s | meromorphicOrderAt (logDeriv f) s < 0} = D.support := by    simpa [R, D] using      logDeriv_poles_eq_divisor_support (f := f) (R := R) hf hlog hfinite_order  have hlog_no_boundary :      Disjoint (RectangleBorder z w) {s | meromorphicOrderAt (logDeriv f) s < 0} := by    rw [Set.disjoint_left]    intro s hs_border hs_log_pole    have hsR : s ∈ R := by      exact rectangleBorder_subset_rectangle z w hs_border    have hsD : s ∈ D.support := by      rw [← hlog_poles_eq]      exact ⟨hsR, hs_log_pole⟩    exact Set.disjoint_left.mp (by simpa [R, D] using hno_boundary) hs_border hsD  have hlog_poles_finite :      (Rectangle z w ∩ {s | meromorphicOrderAt (logDeriv f) s < 0}).Finite := by    simpa [R, D, hlog_poles_eq] using hsupport  have hrect :=    RectangleIntegral'_eq_sumResiduesIn zRe_le_wRe zIm_le_wIm hlog hlog_no_boundary      hlog_poles_finite hlog_simple  rw [hrect, hlog_poles_eq, sumResiduesIn_eq_finset_of_finite hsupport]  refine Finset.sum_congr rfl ?_  intro p hp  have hpD : p ∈ D.support := by    simpa [D] using (hsupport.mem_toFinset.mp hp)  have hpR : p ∈ R := D.supportWithinDomain hpD  have hpD_ne : D p ≠ 0 := by    simpa [Function.mem_support] using hpD  have horder_ne_zero_or_top :      meromorphicOrderAt f p ≠ 0 ∧ meromorphicOrderAt f p ≠ ⊤ := by    change (MeromorphicOn.divisor f R) p ≠ 0 at hpD_ne    rw [MeromorphicOn.divisor_apply hf hpR] at hpD_ne    constructor    · intro hzero      exact hpD_ne (by simp [hzero])    · intro htop      exact hpD_ne (by simp [htop])  obtain ⟨n, hn⟩ :=    WithTop.ne_top_iff_exists.mp horder_ne_zero_or_top.2  have hres :      residue (logDeriv f) p = (n : ℂ) :=    logDeriv_residue_eq_meromorphicOrderAt (hf p hpR) hn.symm  rw [hres]  change (n : ℂ) = ((MeromorphicOn.divisor f R) p : ℂ)  rw [MeromorphicOn.divisor_apply hf hpR, ← hn]  simp