exists_antitone_of_eventually

lemma exists_antitone_of_eventually {u : ℕ → ℝ} (hu : ∀ᶠ n in atTop, u (n + 1) ≤ u n) :    ∃ v : ℕ → ℝ, range v ⊆ range u ∧ Antitone v ∧ v =ᶠ[atTop] u := by  obtain ⟨N, hN⟩ := eventually_atTop.mp hu  let v (n : ℕ) := u (if n < N then N else n)  refine ⟨v, ?_, ?_, ?_⟩  · exact fun x ⟨n, hn⟩ => ⟨if n < N then N else n, hn⟩  · refine antitone_nat_of_succ_le (fun n => ?_)    by_cases h : n < N    · by_cases h' : n + 1 < N <;> simp [v, h, h']      have : n + 1 = N := by linarith      simp [this]    · have : ¬(n + 1 < N) := by linarith      simp only [this, ↓reduceIte, h, ge_iff_le, v] ; apply hN ; linarith  · have : ∀ᶠ n in atTop, ¬(n < N) := by simpa using ⟨N, fun b hb => by linarith⟩    filter_upwards [this] with n hn ; simp [v, hn]