Theorem: RectangleIntegral_tendsTo_LowerU
Proof state before:
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
hvert :
  ∀ (s : ℝ),
    Integrable (fun y => f (↑s + ↑y * I)) volume →
      Tendsto (fun U => I * ∫ (y : ℝ) in -U..-T, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Iic (-T), f (↑s + ↑y * I)))
this :
  Tendsto
    (fun x =>
      (((∫ (x_1 : ℝ) in σ..σ', f (↑x_1 - ↑x * I)) - ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) +
          I * ∫ (y : ℝ) in -x..-T, f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in -x..-T, f (↑σ + ↑y * I))
    atTop
    (𝓝
      (((-∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) + I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)))
⊢ Tendsto
    (fun U =>
      (((∫ (x : ℝ) in σ..σ', f (↑x + -(↑U * I))) - ∫ (x : ℝ) in σ..σ', f (↑x + -(↑T * I))) +
          I • ∫ (y : ℝ) in -U..-T, f (↑σ' + ↑y * I)) -
        I • ∫ (y : ℝ) in -U..-T, f (↑σ + ↑y * I))
    atTop
    (𝓝
      (-(I • ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)) +
        ((I • ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) - ∫ (x : ℝ) in σ..σ', f (↑x + -(↑T * I)))))
Tactic:
have final : (((-∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) + I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) -
    I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)) = (-(I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)) +
    ((I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) - ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I))) := by
  ring_nf
Proof state after:
σ σ' T : ℝ
f : ℂ → ℂ
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h_re : ∀ (s t : ℝ), (↑s - I * ↑t).re = s
h_im : ∀ (s t : ℝ), (↑s - I * ↑t).im = -t
hbot' : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x - ↑y * I)) atTop (𝓝 0)
htop : Tendsto (fun x => ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) atTop (𝓝 (∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)))
hvert :
  ∀ (s : ℝ),
    Integrable (fun y => f (↑s + ↑y * I)) volume →
      Tendsto (fun U => I * ∫ (y : ℝ) in -U..-T, f (↑s + ↑y * I)) atTop (𝓝 (I * ∫ (y : ℝ) in Iic (-T), f (↑s + ↑y * I)))
this :
  Tendsto
    (fun x =>
      (((∫ (x_1 : ℝ) in σ..σ', f (↑x_1 - ↑x * I)) - ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) +
          I * ∫ (y : ℝ) in -x..-T, f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in -x..-T, f (↑σ + ↑y * I))
    atTop
    (𝓝
      (((-∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) + I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) -
        I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)))
final :
  ((-∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) + I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) -
      I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I) =
    -(I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)) +
      ((I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) - ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I))
⊢ Tendsto
    (fun U =>
      (((∫ (x : ℝ) in σ..σ', f (↑x + -(↑U * I))) - ∫ (x : ℝ) in σ..σ', f (↑x + -(↑T * I))) +
          I • ∫ (y : ℝ) in -U..-T, f (↑σ' + ↑y * I)) -
        I • ∫ (y : ℝ) in -U..-T, f (↑σ + ↑y * I))
    atTop
    (𝓝
      (-(I • ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)) +
        ((I • ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) - ∫ (x : ℝ) in σ..σ', f (↑x + -(↑T * I)))))