no goals
ι : Type ?u.75677
ι' : Type ?u.75680
α : Type ?u.75683
β : Type u_1
γ : Type ?u.75689
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
⊢ ∃ᶠ (n : ℕ) in atTop, ∀ (k : ℕ), k < n → u k < u n
simpa [frequently_atTop] using high_scores hu