Theorem: RectangleIntegral'_congr (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₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ RectangleIntegral' f z w = RectangleIntegral' g z w
Tactic:
rw [RectangleIntegral', RectangleIntegral_congr h]
State after:
no goals