have := tendsto_rpow_atTop_nhds_zero_of_norm_lt_one xpos x_lt_one C
case intro.intro
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ
left✝ : C > 0
hC : ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral (f x)) atTop (𝓝 0)
case intro.intro
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ
left✝ : C > 0
hC : ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
this : Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral (f x)) atTop (𝓝 0)