Theorem: RectanglePullToNhdOfPole'' (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₂ σ : ℝ
inst✝ : CompleteSpace E
z w p : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, RectangleIntegral' f z w = RectangleIntegral' f (-↑c - I * ↑c + p) (↑c + I * ↑c + p)
Tactic:
filter_upwards [RectanglePullToNhdOfPole zRe_le_wRe zIm_le_wIm pInRectInterior fHolo] with c h
State after:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f g : ℂ → E
z✝ w✝ p✝ c✝ A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
inst✝ : CompleteSpace E
z w p : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
c : ℝ
h : RectangleIntegral f z w = RectangleIntegral f (-↑c - I * ↑c + p) (↑c + I * ↑c + p)
⊢ RectangleIntegral' f z w = RectangleIntegral' f (-↑c - I * ↑c + p) (↑c + I * ↑c + p)

State before:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f g : ℂ → E
z✝ w✝ p✝ c✝ A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
inst✝ : CompleteSpace E
z w p : ℂ
zRe_le_wRe : z.re ≤ w.re
zIm_le_wIm : z.im ≤ w.im
pInRectInterior : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
c : ℝ
h : RectangleIntegral f z w = RectangleIntegral f (-↑c - I * ↑c + p) (↑c + I * ↑c + p)
⊢ RectangleIntegral' f z w = RectangleIntegral' f (-↑c - I * ↑c + p) (↑c + I * ↑c + p)
Tactic:
simp_rw [RectangleIntegral', h]
State after:
no goals