(conv at hC => intro σ hσ; rw [mul_comm])
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ a < -3 / 2, (⇑Complex.abs ∘ VerticalIntegral' f) a ≤ x ^ a * C
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ < -3 / 2, ‖VerticalIntegral' f σ‖ ≤ x ^ σ * C
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ a < -3 / 2, (⇑Complex.abs ∘ VerticalIntegral' f) a ≤ x ^ a * C