filter_upwards [l1, l2, l3, l5] with x l1 l2 l3 l5
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‖
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
l1✝ : ∀ᶠ (x : ℝ) in atTop, a * x + b ≤ x ^ 2
x : ℝ
l1 : a * x + b ≤ x ^ 2
l2 : 0 ≤ x.log
l3 : 0 ≤ (a * x + b).log
l5 : 1 ≤ a * x + b
⊢ ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖