have h_σ_yI : (fun (σy : ℝ × ℝ) ↦ σy.1 + σy.2 * I) =Θ[l] Prod.snd := by
  refine IsLittleO.add_isTheta ?_ h_yI
  exact continuous_ofReal.continuousOn.const_isBigOUniformlyOn_isCompact isCompact_uIcc
    (by norm_num : ‖(1 : ℂ)‖ ≠ 0) _ |>.trans_isLittleO h_c
case refine_2
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
h_c : ∀ {c : ℂ}, (fun x => c) =o[l] Prod.snd
h_yI :
  (fun x =>
      match x with
      | (_σ, y) => ↑y * I) =Θ[l]
    Prod.snd
⊢ (fun x => (↑x.1 + ↑x.2 * I) * (↑x.1 + ↑x.2 * I + 1)) =Θ[l] fun x => x.2 ^ 2
case refine_2
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
h_c : ∀ {c : ℂ}, (fun x => c) =o[l] Prod.snd
h_yI :
  (fun x =>
      match x with
      | (_σ, y) => ↑y * I) =Θ[l]
    Prod.snd
h_σ_yI : (fun σy => ↑σy.1 + ↑σy.2 * I) =Θ[l] Prod.snd
⊢ (fun x => (↑x.1 + ↑x.2 * I) * (↑x.1 + ↑x.2 * I + 1)) =Θ[l] fun x => x.2 ^ 2