CH2.sumResiduesIn_centralRectangle_eq_sumResiduesIn_RC

lemma sumResiduesIn_centralRectangle_eq_sumResiduesIn_RC (l : LadderParams) (n : ℕ) (G_circ : ℂ → ℂ) (x : ℝ)    (h_rect_mero : MeromorphicOn (fun s ↦ G_circ s * (x : ℂ) ^ s) (Rectangle ((l.σ n : ℂ) - (l.δ : ℂ) * Complex.I) (1 + (l.δ : ℂ) * Complex.I)))    (h_no_poles_boundary : Disjoint (RectangleBorder ((l.σ n : ℂ) - (l.δ : ℂ) * Complex.I) (1 + (l.δ : ℂ) * Complex.I)) {z | meromorphicOrderAt (fun s ↦ G_circ s * (x : ℂ) ^ s) z < 0}) :    sumResiduesIn (fun s ↦ G_circ s * (x : ℂ) ^ s) (Rectangle ((l.σ n : ℂ) - (l.δ : ℂ) * Complex.I) (1 + (l.δ : ℂ) * Complex.I) ∩ {z | meromorphicOrderAt (fun s ↦ G_circ s * (x : ℂ) ^ s) z < 0}) =      sumResiduesIn (fun s ↦ G_circ s * (x : ℂ) ^ s) (l.RC ∩ {z | l.σ n < z.re}) := by  let F := fun s ↦ G_circ s * (x : ℂ) ^ s  let Rn := Rectangle ((l.σ n : ℂ) - (l.δ : ℂ) * Complex.I) (1 + (l.δ : ℂ) * Complex.I)  let P := {z | meromorphicOrderAt F z < 0}  let S2 := l.RC ∩ {z | l.σ n < z.re}  have hnegδ_le_δ : -l.δ ≤ l.δ := by    simpa only [neg_le_self_iff] using l.hδ.1.le  have hRn_mero : MeromorphicOn F Rn := by    simpa [F, Rn] using h_rect_mero  have h_set_eq : Rn ∩ P = S2 ∩ P := by    simpa [F, Rn, P, S2] using      (centralRectangle_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.RC ∩ {z | l.σ n < z.re} := by      simpa [S2] using hs_S2    have hs_im_bounds := abs_le.mp hs_S2'.1.2    change s ∈ Rectangle ((l.σ n : ℂ) - (l.δ : ℂ) * Complex.I) (1 + (l.δ : ℂ) * Complex.I)    rw [mem_Rect (by simpa using l.hσ n) (by simpa using hnegδ_le_δ)]    exact ⟨by simpa using le_of_lt hs_S2'.2, by simpa using hs_S2'.1.1,      by simpa using hs_im_bounds.1, by simpa using hs_im_bounds.2⟩  exact sumResiduesIn_eq_of_inter_poles_eq_and_subset hRn_mero h_set_eq hS2_subset