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_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
hp : 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 [Ioo_mem_nhdsWithin_Ioi' zero_lt_one, SmallSquareInRectangle hp]
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_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
hp : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
⊢ ∀ a ∈ Ioo 0 1,
    Square p a ⊆ Rectangle z w → RectangleIntegral f z w = RectangleIntegral f (-↑a - I * ↑a + p) (↑a + I * ↑a + 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_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
hp : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
⊢ ∀ a ∈ Ioo 0 1,
    Square p a ⊆ Rectangle z w → RectangleIntegral f z w = RectangleIntegral f (-↑a - I * ↑a + p) (↑a + I * ↑a + p)
Tactic:
intro c ⟨cpos, _⟩ hc
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_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
hp : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
c : ℝ
cpos : 0 < c
right✝ : c < 1
hc : Square p c ⊆ Rectangle z w
⊢ 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_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
hp : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
c : ℝ
cpos : 0 < c
right✝ : c < 1
hc : Square p c ⊆ Rectangle z w
⊢ RectangleIntegral f z w = RectangleIntegral f (-↑c - I * ↑c + p) (↑c + I * ↑c + p)
Tactic:
simp_rw [mul_comm I]
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_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
hp : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
c : ℝ
cpos : 0 < c
right✝ : c < 1
hc : Square p c ⊆ Rectangle z w
⊢ RectangleIntegral f z w = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + 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_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
hp : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
c : ℝ
cpos : 0 < c
right✝ : c < 1
hc : Square p c ⊆ Rectangle z w
⊢ RectangleIntegral f z w = RectangleIntegral f (-↑c - ↑c * I + p) (↑c + ↑c * I + p)
Tactic:
exact RectanglePullToNhdOfPole' (by simp_all [cpos.le])
  (square_mem_nhds p (ne_of_gt cpos)) hc fHolo
State after:
no goals

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_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
hp : Rectangle z w ∈ 𝓝 p
fHolo : HolomorphicOn f (Rectangle z w \ {p})
c : ℝ
cpos : 0 < c
right✝ : c < 1
hc : Square p c ⊆ Rectangle z w
⊢ z.re ≤ w.re ∧
    z.im ≤ w.im ∧ (-↑c - ↑c * I + p).re ≤ (↑c + ↑c * I + p).re ∧ (-↑c - ↑c * I + p).im ≤ (↑c + ↑c * I + p).im
Tactic:
simp_all [cpos.le]
State after:
no goals