set l := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop : Filter ℝ) with hl
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
⊢ (fun x_1 =>
      match x_1 with
      | (σ, y) => f x (↑σ + ↑y * I)) =Θ[𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)]
    ((fun y => 1 / y ^ 2) ∘ Prod.snd)
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)