obtain ⟨N, hN⟩ := eventually_atTop.mp hu
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
⊢ ∃ v, range v ⊆ range u ∧ Antitone v ∧ v =ᶠ[atTop] u
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
⊢ ∃ v, range v ⊆ range u ∧ Antitone v ∧ v =ᶠ[atTop] u