no goals
α : Type u_1
β : Type ?u.108288
γ : Type ?u.108291
ι : Type ?u.108294
inst✝ : CompleteLattice α
u : ℕ → α
⊢ limsup u atTop = ⨅ (n : ℕ), ⨆ (i : ℕ), u (i + n)
simp only [limsup_eq_iInf_iSup_of_nat, iSup_ge_eq_iSup_nat_add]