field_simp
n : ℕ
A a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
hb : 0 < b
l1 :
  (nabla fun n => n * (a + (n / b).log ^ 2)) = fun n =>
    a + ((n + 1) / b).log ^ 2 + n * (((n + 1) / b).log ^ 2 - (n / b).log ^ 2)
l2 : (fun x => a) =O[atTop] ((fun x => x ^ 2) ∘ Real.log)
l3 : (fun n => ((n + 1) / b).log ^ 2) =O[atTop] fun n => n.log ^ 2
l4 : (fun x => ((x + 1) / b).log + (x / b).log) =O[atTop] Real.log
x : ℝ
hx : 1 ≤ x
⊢ x * (x.log * (1 / x)) = x.log
no goals