α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ((⨆ (_ : 0 < n + 1), u 0) ⊔ ⨆ (i : ℕ) (_ : i + 1 < n + 1), u (i + 1)) = u 0 ⊔ ⨆ (k : ℕ) (_ : k < n), u (k + 1)
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ (⨆ (k : ℕ) (_ : k < n + 1), u k) = u 0 ⊔ ⨆ (k : ℕ) (_ : k < n), u (k + 1)
rw [← sup_iSup_nat_succ]
no goals
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ((⨆ (_ : 0 < n + 1), u 0) ⊔ ⨆ (i : ℕ) (_ : i + 1 < n + 1), u (i + 1)) = u 0 ⊔ ⨆ (k : ℕ) (_ : k < n), u (k + 1)
simp