CH2.tendsto_contour_shift_downwards

lemma tendsto_contour_shift_downwards {σ σ' : ℝ} {f : ℂ → ℂ}    (hf_anal : ∀ (U : ℝ), U ≥ 0 → HolomorphicOn f (Rectangle (σ : ℂ) (σ' - I * U)))    (h_bottom : Filter.Tendsto (fun (T : ℝ) ↦ ∫ t in σ..σ', f (t - I * T)) Filter.atTop (nhds 0)) :    Filter.Tendsto (fun (T : ℝ) ↦ (I * ∫ t in Set.Icc 0 T, f (σ' - I * t)) - (I * ∫ t in Set.Icc 0 T, f (σ - I * t))) Filter.atTop (nhds (∫ t in σ..σ', f t)) := by  have h_rect (T : ℝ) (hT : 0 ≤ T) :      RectangleIntegral f σ (σ' - I * T) =      (∫ t in σ..σ', f t) - (∫ t in σ..σ', f (t - I * T)) - (I * ∫ t in Set.Icc 0 T, f (σ' - I * t)) + (I * ∫ t in Set.Icc 0 T, f (σ - I * t)) := by    dsimp [RectangleIntegral, HIntegral, VIntegral]    have h1 : ∫ (x : ℝ) in σ..σ' - (0 * T - 1 * 0), f (↑x + 0 * I) = ∫ x in σ..σ', f ↑x := by      simp only [show σ' - (0 * T - 1 * 0) = σ' from by ring]      exact intervalIntegral.integral_congr fun x _ ↦ by ring_nf    have h2 : ∫ (x : ℝ) in σ..σ' - (0 * T - 1 * 0), f (↑x + ↑(0 - (0 * 0 + 1 * T)) * I) = ∫ x in σ..σ', f (↑x - I * ↑T) := by      simp only [show σ' - (0 * T - 1 * 0) = σ' from by ring]      exact intervalIntegral.integral_congr fun x _ ↦ by norm_cast; simp; ring_nf    have h3 : ∫ (y : ℝ) in 0..0 - (0 * 0 + 1 * T), f (↑(σ' - (0 * T - 1 * 0)) + ↑y * I) = - ∫ t in Set.Icc 0 T, f (↑σ' - I * ↑t) := by      rw [show (0 : ℝ) - (0 * 0 + 1 * T) = -T from by ring,          show σ' - (0 * T - 1 * 0) = σ' from by ring, neg_zero.symm]      rw [← intervalIntegral.integral_comp_neg (f := fun y ↦ f (↑σ' + ↑y * I)) (a := T) (b := 0)]      rw [intervalIntegral.integral_symm, intervalIntegral.integral_of_le hT, MeasureTheory.integral_Icc_eq_integral_Ioc]      simp only [neg_zero]      exact congr_arg Neg.neg (integral_congr_ae (Filter.Eventually.of_forall fun y ↦ by push_cast; ring_nf))    have h4 : ∫ (y : ℝ) in 0..0 - (0 * 0 + 1 * T), f (↑σ + ↑y * I) = - ∫ t in Set.Icc 0 T, f (↑σ - I * ↑t) := by      rw [show (0 : ℝ) - (0 * 0 + 1 * T) = -T from by ring, neg_zero.symm]      rw [← intervalIntegral.integral_comp_neg (f := fun y ↦ f (↑σ + ↑y * I)) (a := T) (b := 0)]      rw [intervalIntegral.integral_symm, intervalIntegral.integral_of_le hT, MeasureTheory.integral_Icc_eq_integral_Ioc]      simp only [neg_zero]      exact congr_arg Neg.neg (integral_congr_ae (Filter.Eventually.of_forall fun y ↦ by push_cast; ring_nf))    have h3' : ∫ (y : ℝ) in 0..-T, f (↑σ' + ↑y * I) =        -∫ t in Set.Icc 0 T, f (↑σ' - I * ↑t) := by      simpa [Complex.I_mul_re, Complex.I_mul_im] using h3    have h4' : ∫ (y : ℝ) in 0..-T, f (↑σ + ↑y * I) =        -∫ t in Set.Icc 0 T, f (↑σ - I * ↑t) := by      simpa [Complex.I_mul_im] using h4    rw [← h1, ← h2]    simp only [Complex.I_mul_re, Complex.I_mul_im, Complex.ofReal_re, Complex.ofReal_im,      neg_zero, zero_sub, sub_zero]    rw [h3', h4']    simp    ring   have h_zero : Filter.Tendsto (fun (T : ℝ) ↦ RectangleIntegral f σ (σ' - I * T)) Filter.atTop (nhds 0) :=    tendsto_const_nhds.congr' (by      filter_upwards [Filter.eventually_ge_atTop 0] with T hT      exact (HolomorphicOn.vanishesOnRectangle (hf_anal T hT) subset_rfl).symm)  have h_total_lim : Filter.Tendsto (fun (T : ℝ) ↦ (∫ t in σ..σ', f t) - (∫ t in σ..σ', f (t - I * T)) - RectangleIntegral f σ (σ' - I * T)) Filter.atTop (nhds (∫ t in σ..σ', f t)) := by    simpa only [sub_zero] using ((tendsto_const_nhds (x := ∫ t in σ..σ', f t)).sub h_bottom).sub h_zero  exact h_total_lim.congr' (by    filter_upwards [Filter.eventually_ge_atTop 0] with T hT    rw [h_rect T hT]; ring)