Theorem: Perron.residueAtZero
Proof state before:
case h.intro.intro.intro.refine_1
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
cpos : 0 < c
right✝ : c < 1 / 2
RectSub : Square 0 c \ {0} ⊆ {0, -1}ᶜ
f1Holo : HolomorphicOn (f x - fun s => 1 / s) (Square 0 c \ {0})
g : ℂ → ℂ
g_eq_fDiff : EqOn (f x - fun s => 1 / s) g (Square 0 c \ {0})
fHolo : HolomorphicOn (f x) (Rectangle (-↑c - ↑c * I) (↑c + ↑c * I) \ {0})
gHolo : HolomorphicOn g (Rectangle (-↑c - ↑c * I) (↑c + ↑c * I))
RectMemNhds : Rectangle (-↑c - ↑c * I) (↑c + ↑c * I) ∈ 𝓝 0
⊢ (-↑c - ↑c * I).re ≤ (↑c + ↑c * I).re

case h.intro.intro.intro.refine_2
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
cpos : 0 < c
right✝ : c < 1 / 2
RectSub : Square 0 c \ {0} ⊆ {0, -1}ᶜ
f1Holo : HolomorphicOn (f x - fun s => 1 / s) (Square 0 c \ {0})
g : ℂ → ℂ
g_eq_fDiff : EqOn (f x - fun s => 1 / s) g (Square 0 c \ {0})
fHolo : HolomorphicOn (f x) (Rectangle (-↑c - ↑c * I) (↑c + ↑c * I) \ {0})
gHolo : HolomorphicOn g (Rectangle (-↑c - ↑c * I) (↑c + ↑c * I))
RectMemNhds : Rectangle (-↑c - ↑c * I) (↑c + ↑c * I) ∈ 𝓝 0
⊢ (-↑c - ↑c * I).im ≤ (↑c + ↑c * I).im

case h.intro.intro.intro.refine_3
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
cpos : 0 < c
right✝ : c < 1 / 2
RectSub : Square 0 c \ {0} ⊆ {0, -1}ᶜ
f1Holo : HolomorphicOn (f x - fun s => 1 / s) (Square 0 c \ {0})
g : ℂ → ℂ
g_eq_fDiff : EqOn (f x - fun s => 1 / s) g (Square 0 c \ {0})
fHolo : HolomorphicOn (f x) (Rectangle (-↑c - ↑c * I) (↑c + ↑c * I) \ {0})
gHolo : HolomorphicOn g (Rectangle (-↑c - ↑c * I) (↑c + ↑c * I))
RectMemNhds : Rectangle (-↑c - ↑c * I) (↑c + ↑c * I) ∈ 𝓝 0
⊢ EqOn (f x - fun s => 1 / (s - 0)) g (Rectangle (-↑c - ↑c * I) (↑c + ↑c * I) \ {0})
Tactic:
any_goals simpa using cpos.le
Proof state after:
case h.intro.intro.intro.refine_3
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
cpos : 0 < c
right✝ : c < 1 / 2
RectSub : Square 0 c \ {0} ⊆ {0, -1}ᶜ
f1Holo : HolomorphicOn (f x - fun s => 1 / s) (Square 0 c \ {0})
g : ℂ → ℂ
g_eq_fDiff : EqOn (f x - fun s => 1 / s) g (Square 0 c \ {0})
fHolo : HolomorphicOn (f x) (Rectangle (-↑c - ↑c * I) (↑c + ↑c * I) \ {0})
gHolo : HolomorphicOn g (Rectangle (-↑c - ↑c * I) (↑c + ↑c * I))
RectMemNhds : Rectangle (-↑c - ↑c * I) (↑c + ↑c * I) ∈ 𝓝 0
⊢ EqOn (f x - fun s => 1 / (s - 0)) g (Rectangle (-↑c - ↑c * I) (↑c + ↑c * I) \ {0})