have : Finset.sup Finset.univ (fun i => f (Fin.succ i)) = Finset.sup {0}ᶜ f := by
  simpa[Function.comp] using Eq.symm <| Finset.sup_image (Finset.univ : Finset (Fin n)) Fin.succ f
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = f 0 ⊔ {0}ᶜ.sup f
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this✝ : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
this : (Finset.univ.sup fun i => f i.succ) = {0}ᶜ.sup f
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = f 0 ⊔ {0}ᶜ.sup f