have l1 : ∀ᶠ x : ℝ in atTop, a * x + b ≤ x ^ 2 := by
  filter_upwards [(isLittleO_mul_add_sq a b).eventuallyLE, l5] with x r2 l5
  simpa [abs_eq_self.mpr (zero_le_one.trans l5)] using r2
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5 : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5 : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
l1 : ∀ᶠ (x : ℝ) in atTop, a * x + b ≤ x ^ 2
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖