have hcast : (fun (y : ℝ) ↦ 1 / y ^ 2) =ᶠ[atTop] fun y ↦ y ^ (-2 : ℝ) := by
  filter_upwards [Ici_mem_atTop 0] with y hy using by rw [rpow_neg hy, inv_eq_one_div, rpow_two]
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
⊢ Tendsto (fun t => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑t * I)) atTop (𝓝 0)
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
hcast : (fun y => 1 / y ^ 2) =ᶠ[atTop] fun y => y ^ (-2)
⊢ Tendsto (fun t => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑t * I)) atTop (𝓝 0)