have h_c {c : ℂ} : (fun (_ : ℝ × ℝ) ↦ c) =o[l] Prod.snd := by
  rewrite [hl, Filter.prod_sup, isLittleO_sup]
  exact ⟨isLittleO_const_snd_atBot c _, isLittleO_const_snd_atTop c _⟩
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
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
⊢ (fun x => (↑x.1 + ↑x.2 * I) * (↑x.1 + ↑x.2 * I + 1)) =Θ[l] fun x => x.2 ^ 2