RectangleIntegral'_eq_sumResiduesIn

lemma RectangleIntegral'_eq_sumResiduesIn {f : ℂ → ℂ} {z w : ℂ}    (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im)    (f_mero : MeromorphicOn f (Rectangle z w))    (f_no_poles_boundary : Disjoint (RectangleBorder z w) {z | meromorphicOrderAt f z < 0})    (f_poles_finite : (Rectangle z w ∩ {z | meromorphicOrderAt f z < 0}).Finite)    (f_simple_poles : HasSimplePolesOn f (Rectangle z w)) :    RectangleIntegral' f z w = sumResiduesIn f (Rectangle z w ∩ {z | meromorphicOrderAt f z < 0}) := by  let R : Set ℂ := Rectangle z w  let poles : Set ℂ := R ∩ {u | meromorphicOrderAt f u < 0}  let polesFin : Finset ℂ := f_poles_finite.toFinset  let fNF : ℂ → ℂ := toMeromorphicNFOn f R  let principalPart : ℂ → ℂ := fun s ↦ ∑ p ∈ polesFin, residue fNF p / (s - p)  let holoPart : ℂ → ℂ := toMeromorphicNFOn (fNF - principalPart) R  have h_residue_congr : sumResiduesIn f poles = sumResiduesIn fNF poles := by    rw [sumResiduesIn, sumResiduesIn]    apply tsum_congr    intro p    exact (residue_toMeromorphicNFOn_eq_residue p.2.1 f_mero f_simple_poles p.2.2).symm  have h_principalPart_integral : RectangleIntegral' principalPart z w = sumResiduesIn fNF poles := by    have h_sum : RectangleIntegral' principalPart z w = ∑ p ∈ polesFin, residue fNF p := by      apply rectangleIntegral'_sum_div_sub zRe_le_wRe zIm_le_wIm      · intro p hp        dsimp [polesFin, poles, R] at hp        simp only [Finset.mem_coe, Set.Finite.mem_toFinset] at hp        exact hp.1      · exact Disjoint.mono_right (by rw [f_poles_finite.coe_toFinset]; exact Set.inter_subset_right) f_no_poles_boundary    rw [h_sum]    have h_eq_poles : poles = ↑polesFin := by      dsimp [poles, polesFin, R]      exact f_poles_finite.coe_toFinset.symm    rw [sumResiduesIn, h_eq_poles,      tsum_fintype (f := fun p : (polesFin : Set ℂ) => residue fNF p),      ← Finset.sum_coe_sort polesFin]; rfl  calc    RectangleIntegral' f z w = RectangleIntegral' fNF z w := rectangleIntegral'_toMeromorphicNFOn_eq f_mero    _ = RectangleIntegral' holoPart z w + RectangleIntegral' principalPart z w :=      toMeromorphicNFOn_add_integral f_mero f_no_poles_boundary f_poles_finite f_simple_poles    _ = 0 + sumResiduesIn fNF poles := by      rw [h_principalPart_integral]      rw [RectangleIntegral',        (holoPart_holomorphicOn f_mero f_simple_poles f_poles_finite).vanishesOnRectangle subset_rfl]      simp    _ = sumResiduesIn fNF poles := by simp    _ = sumResiduesIn f poles := h_residue_congr.symm