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', RectangleIntegral.translate]
State after:
no goals