have l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] (fun n => (n * (Real.log n) ^ 2)⁻¹) := by
  refine IsBigO.trans ?_ l4
  rw [isBigO_iff] ; use 1
  have e1 : ∀ᶠ n in atTop, 0 < d n := by
    apply eventually_of_mem (Ici_mem_atTop 1) ; intro n (hn : 1 ≤ n)
    have r1 : 0 < n := by linarith
    have r2 : 0 < (2 * π) ^ 2 := by apply sq_pos_of_ne_zero ; norm_num [pi_ne_zero]
    have r3 : 0 ≤ Real.log (↑n / x) ^ 2 := sq_nonneg _
    apply mul_pos r1 (by linarith)
  have e2 : ∀ᶠ n in atTop, 0 < d (n + 1) := (tendsto_atTop_add_const_right atTop (1 : ℝ) tendsto_id).eventually e1
  have e3 : ∀ᶠ n in atTop, d n ≤ d (n + 1) := by
    have : ∀ᶠ n in atTop, x ≤ n := by simpa using eventually_ge_atTop x
    filter_upwards [this] with n hn
    have e2 : 1 ≤ n / x := (one_le_div (by linarith)).mpr hn
    have e3 : n ≤ n + 1 := by linarith
    have e4 : 0 ≤ n + 1 := by linarith
    dsimp [d]
    gcongr
    exact Real.log_nonneg e2
  filter_upwards [e1, e2, e3] with n e1 e2 e3
  simp_rw [one_mul, Real.norm_eq_abs, abs_inv, abs_eq_self.mpr e1.le, abs_eq_self.mpr e2.le, inv_le_inv e2 e1]
  exact e3
n : ℕ
A a b c d✝ u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
d : ℝ → ℝ := fun n => n * ((2 * π) ^ 2 + (n / x).log ^ 2)
l2 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
l3 : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
l1 : ∀ᶠ (n : ℝ) in atTop, nnabla (fun n => 1 / d n) n = (d (n + 1) - d n) * (d n)⁻¹ * (d (n + 1))⁻¹
l4 : (fun n => (d n)⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
⊢ (fun x_1 => nnabla (fun n => 1 / d n) x_1) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)
n : ℕ
A a b c d✝ u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
d : ℝ → ℝ := fun n => n * ((2 * π) ^ 2 + (n / x).log ^ 2)
l2 : ∀ᶠ (n : ℝ) in atTop, 0 < d n
l3 : ∀ᶠ (n : ℝ) in atTop, 0 < d (n + 1)
l1 : ∀ᶠ (n : ℝ) in atTop, nnabla (fun n => 1 / d n) n = (d (n + 1) - d n) * (d n)⁻¹ * (d (n + 1))⁻¹
l4 : (fun n => (d n)⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
l5 : (fun n => (d (n + 1))⁻¹) =O[atTop] fun n => (n * n.log ^ 2)⁻¹
⊢ (fun x_1 => nnabla (fun n => 1 / d n) x_1) =O[atTop] fun n => 1 / (n.log ^ 2 * n ^ 2)