no goals
α : Type u_1
β : Type ?u.180415
β₂ : Type ?u.180418
γ : Type ?u.180421
ι : Sort ?u.180424
ι' : Sort ?u.180427
κ : ι → Sort ?u.180432
κ' : ι' → Sort ?u.180437
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
⊢ (⨆ (x : ℕ) (_ : x ∈ {0} ∪ range Nat.succ), u x) = ⨆ (i : ℕ), u i
rw [Nat.zero_union_range_succ, iSup_univ]