CH2.sumResiduesIn_upperRectangle_eq_sumResiduesIn_Rpos

lemma sumResiduesIn_upperRectangle_eq_sumResiduesIn_Rpos (l : LadderParams) (n : ℕ) (F : ℂ → ℂ)    (h_rect_mero : MeromorphicOn F (Rectangle ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I)))    (h_no_poles_boundary : Disjoint (RectangleBorder ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I))      {z | meromorphicOrderAt F z < 0}) :    sumResiduesIn F (Rectangle ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I) ∩ {z | meromorphicOrderAt F z < 0}) =      sumResiduesIn F (l.Rpos ∩ {z | l.σ n < z.re}) := by  let Rn : Set ℂ :=    Rectangle ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I)  let P : Set ℂ := {z | meromorphicOrderAt F z < 0}  let S2 : Set ℂ := l.Rpos ∩ {z | l.σ n < z.re}  have hδ_le_T : l.δ ≤ l.T := by linarith [l.hδ.2, l.hT]  have hRn_mero : MeromorphicOn F Rn := by    simpa [Rn] using h_rect_mero  have h_set_eq : Rn ∩ P = S2 ∩ P := by    simpa [Rn, P, S2] using      (upperRectangle_inter_poles_eq (l := l) (n := n) (P := P) h_no_poles_boundary)  have hS2_subset : S2 ⊆ Rn := by    intro s hs_S2    have hs_S2' : s ∈ l.Rpos ∩ {z | l.σ n < z.re} := by      simpa [S2] using hs_S2    rw [show Rn = Rectangle ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I) by      rfl]    rw [mem_Rect (by simpa using l.hσ n) (by simpa using hδ_le_T)]    exact ⟨by simpa using le_of_lt hs_S2'.2, by simpa using hs_S2'.1.1,      by simpa using hs_S2'.1.2.1, by simpa using hs_S2'.1.2.2⟩  exact sumResiduesIn_eq_of_inter_poles_eq_and_subset hRn_mero h_set_eq hS2_subset