simpa [abs_eq_self.mpr (zero_le_one.trans l5)] using r2
case h
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 : ℝ
r2 : ‖a * x + b‖ ≤ ‖x ^ 2‖
l5 : 1 ≤ a * x + b
⊢ a * x + b ≤ x ^ 2
no goals