CH2.intVSeg_eq_intCnPlus_add_rectangleIntegral

lemma intVSeg_eq_intCnPlus_add_rectangleIntegral (l : LadderParams) (n : ℕ) (F : ℂ → ℂ)    (h_integrable1 : IntervalIntegrable (fun t : ℝ ↦ F (1 + t * Complex.I) * Complex.I) volume 0 l.δ)    (h_integrable2 : IntervalIntegrable (fun t : ℝ ↦ F (1 + t * Complex.I) * Complex.I) volume l.δ l.T) :    intVSeg 1 0 l.T F = l.intCnPlus n F + RectangleIntegral F ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I) := by  have h1 : l.intCnPlus n F = (intVSeg 1 0 l.δ F + intHSeg l.δ 1 (l.σ n) F + intVSeg (l.σ n) l.δ l.T F + intHSeg l.T (l.σ n) 1 F) := rfl  have h2 : RectangleIntegral F ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I) = (intHSeg l.δ (l.σ n) 1 F - intHSeg l.T (l.σ n) 1 F + intVSeg 1 l.δ l.T F - intVSeg (l.σ n) l.δ l.T F) := by    have hH1 : HIntegral F (l.σ n) 1 l.δ = intHSeg l.δ (l.σ n) 1 F := rfl    have hH2 : HIntegral F (l.σ n) 1 l.T = intHSeg l.T (l.σ n) 1 F := rfl    have hV1 : Complex.I * ∫ (y : ℝ) in l.δ..l.T, F (1 + ↑y * Complex.I) =      intVSeg 1 l.δ l.T F := by      rw [intVSeg, ← smul_eq_mul, ← intervalIntegral.integral_smul]      refine intervalIntegral.integral_congr (fun y _ ↦ ?_)      rw [smul_eq_mul, mul_comm]; rfl    have hV2 : Complex.I * ∫ (y : ℝ) in l.δ..l.T, F (↑(l.σ n) + ↑y * Complex.I) =      intVSeg (l.σ n) l.δ l.T F := by      rw [intVSeg, ← smul_eq_mul, ← intervalIntegral.integral_smul]      refine intervalIntegral.integral_congr (fun y _ ↦ ?_)      rw [smul_eq_mul, mul_comm]    rw [RectangleIntegral]    simp only [Complex.add_re, Complex.add_im, Complex.mul_re, Complex.mul_im,      Complex.ofReal_re, Complex.ofReal_im, Complex.I_re, Complex.I_im, Complex.one_re,      Complex.one_im, mul_zero, sub_zero, add_zero, mul_one, zero_add]    dsimp [VIntegral]    rw [hH1, hH2, hV1, hV2]  have h_unfolded : l.intCnPlus n F +    RectangleIntegral F ((l.σ n : ℂ) + (l.δ : ℂ) * Complex.I) (1 + (l.T : ℂ) * Complex.I) =    (intVSeg 1 0 l.δ F + intHSeg l.δ 1 (l.σ n) F +     intVSeg (l.σ n) l.δ l.T F + intHSeg l.T (l.σ n) 1 F) +    (intHSeg l.δ (l.σ n) 1 F - intHSeg l.T (l.σ n) 1 F +     intVSeg 1 l.δ l.T F - intVSeg (l.σ n) l.δ l.T F) := by      rw [h1, h2]  have h_δ_cancel : intHSeg l.δ 1 (l.σ n) F + intHSeg l.δ (l.σ n) 1 F = 0 := by    rw [intHSeg, intHSeg, intervalIntegral.integral_symm]    ring  have h_cancelled : (intVSeg 1 0 l.δ F + intHSeg l.δ 1 (l.σ n) F +     intVSeg (l.σ n) l.δ l.T F + intHSeg l.T (l.σ n) 1 F) +    (intHSeg l.δ (l.σ n) 1 F - intHSeg l.T (l.σ n) 1 F +     intVSeg 1 l.δ l.T F - intVSeg (l.σ n) l.δ l.T F) =    intVSeg 1 0 l.δ F + intVSeg 1 l.δ l.T F := by      calc        _ = (intVSeg 1 0 l.δ F + intVSeg 1 l.δ l.T F) +            (intHSeg l.δ 1 (l.σ n) F + intHSeg l.δ (l.σ n) 1 F) := by ring        _ = intVSeg 1 0 l.δ F + intVSeg 1 l.δ l.T F := by rw [h_δ_cancel, add_zero]  have h_adjacent : intVSeg 1 0 l.δ F + intVSeg 1 l.δ l.T F =    intVSeg 1 0 l.T F := by      rw [intVSeg, intVSeg, intVSeg]; push_cast      rw [intervalIntegral.integral_add_adjacent_intervals h_integrable1 h_integrable2]  rw [h_unfolded, h_cancelled, h_adjacent]