no goals
ι : Type ?u.60772
ι' : Type ?u.60775
α : Type ?u.60778
β : Type ?u.60781
γ : Type ?u.60784
P : ℕ → ℕ → Prop
h : ∀ (n : ℕ), ∃ N, ∀ (k : ℕ), k ≥ N → P n k
⊢ ∀ (n : ℕ), ∀ᶠ (k : ℕ) in atTop, P n k
simp [eventually_atTop, h]