Theorem: Perron.residueAtZero (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Tactic:
filter_upwards [Ioo_mem_nhdsWithin_Ioi' (by linarith : (0 : ℝ) < 1 / 2), diffBddAtZero xpos]
State after:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
⊢ ∀ a ∈ Ioo 0 (1 / 2),
    BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 a \ {0})) →
      RectangleIntegral' (f x) (-↑a - ↑a * I) (↑a + ↑a * I) = 1

State before:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
⊢ ∀ a ∈ Ioo 0 (1 / 2),
    BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 a \ {0})) →
      RectangleIntegral' (f x) (-↑a - ↑a * I) (↑a + ↑a * I) = 1
Tactic:
intro c hc bddAbove
State after:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
hc : c ∈ Ioo 0 (1 / 2)
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1

State before:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
c : ℝ
hc : c ∈ Ioo 0 (1 / 2)
bddAbove : BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Tactic:
obtain ⟨cpos, _⟩ := hc
State after:
case h.intro
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
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1

State before:
case h.intro
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
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Tactic:
have RectSub : Square 0 c \ {0} ⊆ {0, -1}ᶜ := by
  refine fun s ⟨hs, hs0⟩ ↦ not_or.mpr ⟨hs0, ?_⟩
  rw [Square, mem_Rect (by simpa using by linarith) (by simp [cpos.le])] at hs
  replace hs : -c ≤ s.re ∧ s.re ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c := by simpa using hs
  simpa [Complex.ext_iff] using fun h ↦ by linarith
State after:
case h.intro
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}ᶜ
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1

State before:
case h.intro
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}ᶜ
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Tactic:
have fHolo : HolomorphicOn (f x) (Square 0 c \ {0}) := (isHolomorphicOn xpos).mono RectSub
State after:
case h.intro
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}ᶜ
fHolo : HolomorphicOn (f x) (Square 0 c \ {0})
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1

State before:
case h.intro
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}ᶜ
fHolo : HolomorphicOn (f x) (Square 0 c \ {0})
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Tactic:
have f1Holo : HolomorphicOn ((f x) - (fun (s : ℂ) ↦ 1 / s)) (Square 0 c \ {0}) :=
  fHolo.sub (by simpa using differentiableOn_inv.mono fun s hs ↦ hs.2)
State after:
case h.intro
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}ᶜ
fHolo : HolomorphicOn (f x) (Square 0 c \ {0})
f1Holo : HolomorphicOn (f x - fun s => 1 / s) (Square 0 c \ {0})
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1

State before:
case h.intro
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}ᶜ
fHolo : HolomorphicOn (f x) (Square 0 c \ {0})
f1Holo : HolomorphicOn (f x - fun s => 1 / s) (Square 0 c \ {0})
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Tactic:
have RectMemNhds : Square 0 c ∈ 𝓝 0 := square_mem_nhds 0 (ne_of_gt cpos)
State after:
case h.intro
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}ᶜ
fHolo : HolomorphicOn (f x) (Square 0 c \ {0})
f1Holo : HolomorphicOn (f x - fun s => 1 / s) (Square 0 c \ {0})
RectMemNhds : Square 0 c ∈ 𝓝 0
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1

State before:
case h.intro
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}ᶜ
fHolo : HolomorphicOn (f x) (Square 0 c \ {0})
f1Holo : HolomorphicOn (f x - fun s => 1 / s) (Square 0 c \ {0})
RectMemNhds : Square 0 c ∈ 𝓝 0
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Tactic:
obtain ⟨g, gHolo, g_eq_fDiff⟩ := existsDifferentiableOn_of_bddAbove RectMemNhds f1Holo bddAbove
State after:
case h.intro.intro.intro
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}ᶜ
fHolo : HolomorphicOn (f x) (Square 0 c \ {0})
f1Holo : HolomorphicOn (f x - fun s => 1 / s) (Square 0 c \ {0})
RectMemNhds : Square 0 c ∈ 𝓝 0
g : ℂ → ℂ
gHolo : HolomorphicOn g (Square 0 c)
g_eq_fDiff : EqOn (f x - fun s => 1 / s) g (Square 0 c \ {0})
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1

State before:
case h.intro.intro.intro
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}ᶜ
fHolo : HolomorphicOn (f x) (Square 0 c \ {0})
f1Holo : HolomorphicOn (f x - fun s => 1 / s) (Square 0 c \ {0})
RectMemNhds : Square 0 c ∈ 𝓝 0
g : ℂ → ℂ
gHolo : HolomorphicOn g (Square 0 c)
g_eq_fDiff : EqOn (f x - fun s => 1 / s) g (Square 0 c \ {0})
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Tactic:
simp_rw [Square, add_zero] at fHolo gHolo RectMemNhds
State after:
case h.intro.intro.intro
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
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1

State before:
case h.intro.intro.intro
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
⊢ RectangleIntegral' (f x) (-↑c - ↑c * I) (↑c + ↑c * I) = 1
Tactic:
refine ResidueTheoremOnRectangleWithSimplePole ?_ ?_ RectMemNhds gHolo ?_
State after:
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})

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
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})

State before:
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:
convert g_eq_fDiff using 3 <;> simp [Square]
State after:
no goals

State before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
xpos : 0 < x
⊢ 0 < 1 / 2
Tactic:
linarith
State after:
no goals

State before:
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
⊢ Square 0 c \ {0} ⊆ {0, -1}ᶜ
Tactic:
refine fun s ⟨hs, hs0⟩ ↦ not_or.mpr ⟨hs0, ?_⟩
State after:
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
s : ℂ
x✝ : s ∈ Square 0 c \ {0}
hs : s ∈ Square 0 c
hs0 : s ∉ {0}
⊢ s ∉ {-1}

State before:
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
s : ℂ
x✝ : s ∈ Square 0 c \ {0}
hs : s ∈ Square 0 c
hs0 : s ∉ {0}
⊢ s ∉ {-1}
Tactic:
rw [Square, mem_Rect (by simpa using by linarith) (by simp [cpos.le])] at hs
State after:
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
s : ℂ
x✝ : s ∈ Square 0 c \ {0}
hs :
  (-↑c - ↑c * I + 0).re ≤ s.re ∧
    s.re ≤ (↑c + ↑c * I + 0).re ∧ (-↑c - ↑c * I + 0).im ≤ s.im ∧ s.im ≤ (↑c + ↑c * I + 0).im
hs0 : s ∉ {0}
⊢ s ∉ {-1}

State before:
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
s : ℂ
x✝ : s ∈ Square 0 c \ {0}
hs :
  (-↑c - ↑c * I + 0).re ≤ s.re ∧
    s.re ≤ (↑c + ↑c * I + 0).re ∧ (-↑c - ↑c * I + 0).im ≤ s.im ∧ s.im ≤ (↑c + ↑c * I + 0).im
hs0 : s ∉ {0}
⊢ s ∉ {-1}
Tactic:
replace hs : -c ≤ s.re ∧ s.re ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c := by simpa using hs
State after:
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
s : ℂ
x✝ : s ∈ Square 0 c \ {0}
hs0 : s ∉ {0}
hs : -c ≤ s.re ∧ s.re ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
⊢ s ∉ {-1}

State before:
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
s : ℂ
x✝ : s ∈ Square 0 c \ {0}
hs0 : s ∉ {0}
hs : -c ≤ s.re ∧ s.re ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
⊢ s ∉ {-1}
Tactic:
simpa [Complex.ext_iff] using fun h ↦ by linarith
State after:
no goals

State before:
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
s : ℂ
x✝ : s ∈ Square 0 c \ {0}
hs : s ∈ Rectangle (-↑c - ↑c * I + 0) (↑c + ↑c * I + 0)
hs0 : s ∉ {0}
⊢ (-↑c - ↑c * I + 0).re ≤ (↑c + ↑c * I + 0).re
Tactic:
simpa using by linarith
State after:
no goals

State before:
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
s : ℂ
x✝ : s ∈ Square 0 c \ {0}
hs : s ∈ Rectangle (-↑c - ↑c * I + 0) (↑c + ↑c * I + 0)
hs0 : s ∉ {0}
⊢ 0 ≤ c
Tactic:
linarith
State after:
no goals

State before:
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
s : ℂ
x✝ : s ∈ Square 0 c \ {0}
hs : s ∈ Rectangle (-↑c - ↑c * I + 0) (↑c + ↑c * I + 0)
hs0 : s ∉ {0}
⊢ (-↑c - ↑c * I + 0).im ≤ (↑c + ↑c * I + 0).im
Tactic:
simp [cpos.le]
State after:
no goals

State before:
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
s : ℂ
x✝ : s ∈ Square 0 c \ {0}
hs :
  (-↑c - ↑c * I + 0).re ≤ s.re ∧
    s.re ≤ (↑c + ↑c * I + 0).re ∧ (-↑c - ↑c * I + 0).im ≤ s.im ∧ s.im ≤ (↑c + ↑c * I + 0).im
hs0 : s ∉ {0}
⊢ -c ≤ s.re ∧ s.re ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
Tactic:
simpa using hs
State after:
no goals

State before:
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
s : ℂ
x✝ : s ∈ Square 0 c \ {0}
hs0 : s ∉ {0}
hs : -c ≤ s.re ∧ s.re ≤ c ∧ -c ≤ s.im ∧ s.im ≤ c
h : s.re = -1
⊢ ¬s.im = 0
Tactic:
linarith
State after:
no goals

State before:
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}ᶜ
fHolo : HolomorphicOn (f x) (Square 0 c \ {0})
⊢ DifferentiableOn ℂ (fun y => (fun s => 1 / s) y) (Square 0 c \ {0})
Tactic:
simpa using differentiableOn_inv.mono fun s hs ↦ hs.2
State after:
no goals

State before:
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:
simpa using cpos.le
State after:
no goals