CH2.upperRectangle_meromorphicOn

lemma upperRectangle_meromorphicOn (n : ℕ)    (hG : ∀ s, G s = G_circ s + (Real.sign s.im : ℂ) * G_star s)    (hG_circ_mero : MeromorphicOn G_circ l.R) (hG_star_mero : MeromorphicOn G_star l.R)    (hx₀ : 1 ≤ x₀) (hx : x₀ < x) :    MeromorphicOn (fun s ↦ G s * (x : ℂ) ^ s)      (Rectangle ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I)) := by  intro s hs  have h_rect_subset_Rpos :      Rectangle ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I) ⊆ l.Rpos :=    l.upperRectangle_subset_Rpos n  have h_rect_subset_R :      Rectangle ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I) ⊆ l.R :=    Set.Subset.trans h_rect_subset_Rpos l.Rpos_subset_R  have hs_Rpos : s ∈ l.Rpos := h_rect_subset_Rpos hs  have hs_R : s ∈ l.R := h_rect_subset_R hs  have hs_im_pos : 0 < s.im := lt_of_lt_of_le l.hδ.1 hs_Rpos.2.1  have h_eq :      (fun t : ℂ ↦ G t * (x : ℂ) ^ t) =ᶠ[nhdsWithin s {s}ᶜ]        (fun t : ℂ ↦ (G_circ t + G_star t) * (x : ℂ) ^ t) := by    have heq : G =ᶠ[nhdsWithin s {s}ᶜ] G_circ + G_star :=      (filter_eventuallyEq_G_pos hG hs_im_pos).filter_mono nhdsWithin_le_nhds    filter_upwards [heq] with t ht    rw [ht]; rfl  refine MeromorphicAt.congr ?_ h_eq.symm  have hx_pos : 0 < x := by linarith  exact ((hG_circ_mero s hs_R).add (hG_star_mero s hs_R)).mul (meromorphicAt_rpow hx_pos s)