refine (𝓟 (uIoc σ' σ'')).eq_or_neBot.casesOn (fun hbot ↦ by simp [hbot]) (fun _ ↦ ?_)
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
⊢ (fun x_1 =>
      match x_1 with
      | (σ, y) => f x (↑σ + ↑y * I)) =Θ[𝓟 (Ι σ' σ'') ×ˢ (atBot ⊔ atTop)]
    fun x =>
    match x with
    | (σ, y) => 1 / y ^ 2
x✝¹ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
x✝ : (𝓟 (Ι σ' σ'')).NeBot
⊢ (fun x_1 =>
      match x_1 with
      | (σ, y) => f x (↑σ + ↑y * I)) =Θ[𝓟 (Ι σ' σ'') ×ˢ (atBot ⊔ atTop)]
    fun x =>
    match x with
    | (σ, y) => 1 / y ^ 2