field_simp
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (fun x_1 => nnabla (fun n => n⁻¹ * ((2 * π) ^ 2 + (n * x⁻¹).log ^ 2)⁻¹) x_1) =O[atTop] fun n =>
    (n.log ^ 2)⁻¹ * (n ^ 2)⁻¹
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 0 < x
⊢ (fun x_1 => nnabla (fun n => 1 / (n * ((2 * π) ^ 2 + (n / x).log ^ 2))) x_1) =O[atTop] fun n =>
    1 / (n.log ^ 2 * n ^ 2)