refine IsTheta.div (isTheta_norm_left.mp ?_) ?_
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
⊢ (fun x_1 =>
      match x_1 with
      | (σ, y) => f x (↑σ + ↑y * I)) =Θ[l]
    ((fun y => 1 / y ^ 2) ∘ Prod.snd)
case refine_1
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
⊢ (fun x_1 => ‖↑x ^ (↑x_1.1 + ↑x_1.2 * I)‖) =Θ[l] fun x => 1

case refine_2
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
⊢ (fun x => (↑x.1 + ↑x.2 * I) * (↑x.1 + ↑x.2 * I + 1)) =Θ[l] fun x => x.2 ^ 2