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

State before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) σ' = VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) σ''
Tactic:
unfold VerticalIntegral'
State after:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ (1 / (2 * ↑π * I)) • VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ' =
    (1 / (2 * ↑π * I)) • VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ''

State before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ (1 / (2 * ↑π * I)) • VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ' =
    (1 / (2 * ↑π * I)) • VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ''
Tactic:
congr 1
State after:
case e_a
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ' = VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ''

State before:
case e_a
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ' = VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ''
Tactic:
exact contourPull (by linarith) (not_mem_uIcc_of_gt (by linarith) (by linarith))
  (not_mem_uIcc_of_gt (by linarith) (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 α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ 0 < x
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 α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ σ' < 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 α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ σ'' < 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 α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ σ' < -1
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 α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ σ'' < -1
Tactic:
linarith
State after:
no goals