CH2.centralRectangle_subset_RC

lemma centralRectangle_subset_RC (l : LadderParams) (n : ℕ) :    Rectangle ((l.σ n : ℂ) - (l.δ : ℂ) * Complex.I) (1 + (l.δ : ℂ) * Complex.I) ⊆ l.RC := by  intro z hz  rcases (mem_Rect      (z := ((l.σ n : ℂ) - (l.δ : ℂ) * Complex.I))      (w := (1 + (l.δ : ℂ) * Complex.I))      (p := z)      (zRe_lt_wRe := by simpa using l.hσ n)      (zIm_lt_wIm := by        simpa only [Complex.sub_im, Complex.add_im, Complex.mul_im, Complex.ofReal_re,          Complex.ofReal_im, Complex.one_im, Complex.I_re, Complex.I_im, zero_mul, mul_zero,          zero_add, add_zero, zero_sub, sub_zero, one_mul, mul_one, neg_le_self_iff] using          l.hδ.1.le)).1 hz with    ⟨_, hz_re_right, hz_im_low, hz_im_high⟩  simp only [LadderParams.RC, Set.mem_setOf_eq]  refine ⟨by simpa using hz_re_right, ?_⟩  exact abs_le.mpr ⟨by simpa using hz_im_low, by simpa using hz_im_high⟩