Theorem: RectangleIntegral.translate (PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g : ℂ → E
z✝ w✝ p✝ c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f : ℂ → E
z w p : ℂ
⊢ RectangleIntegral (fun s => f (s - p)) z w = RectangleIntegral f (z - p) (w - p)
Tactic:
simp_rw [RectangleIntegral, HIntegral, VIntegral, sub_re, sub_im, ← intervalIntegral.integral_comp_sub_right]
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g : ℂ → E
z✝ w✝ p✝ c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f : ℂ → E
z w p : ℂ
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I - p)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I - p)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I - p)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I - p) =
    (((∫ (x : ℝ) in z.re..w.re, f (↑(x - p.re) + ↑(z.im - p.im) * I)) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(x - p.re) + ↑(w.im - p.im) * I)) +
        I • ∫ (x : ℝ) in z.im..w.im, f (↑(w.re - p.re) + ↑(x - p.im) * I)) -
      I • ∫ (x : ℝ) in z.im..w.im, f (↑(z.re - p.re) + ↑(x - p.im) * I)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g : ℂ → E
z✝ w✝ p✝ c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f : ℂ → E
z w p : ℂ
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I - p)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I - p)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I - p)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I - p) =
    (((∫ (x : ℝ) in z.re..w.re, f (↑(x - p.re) + ↑(z.im - p.im) * I)) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(x - p.re) + ↑(w.im - p.im) * I)) +
        I • ∫ (x : ℝ) in z.im..w.im, f (↑(w.re - p.re) + ↑(x - p.im) * I)) -
      I • ∫ (x : ℝ) in z.im..w.im, f (↑(z.re - p.re) + ↑(x - p.im) * I)
Tactic:
congr <;> ext <;> congr 1 <;> simp [Complex.ext_iff]
State after:
no goals