refine this.locallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
  (univ_mem' fun y ↦ ?_) (isTheta xpos).2.isBigO ⟨Ioi 1, Ioi_mem_atTop 1, ?_⟩
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
⊢ Integrable (fun t => f x (↑σ + ↑t * I)) volume
case refine_1
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
y : ℝ
⊢ y ∈
    {x_1 |
      (fun x_2 =>
          (Norm.norm ∘ fun y => f x (↑σ + ↑y * I)) x_2 = (Norm.norm ∘ (fun y => f x (↑σ + ↑y * I)) ∘ Neg.neg) x_2)
        x_1}

case refine_2
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
⊢ IntegrableOn (fun y => 1 / y ^ 2) (Ioi 1) volume