{ simp[ih]
  have : (Finset.univ : Finset (Fin (n + 1))) = insert 0 ((Finset.univ : Finset (Fin n)).image Fin.succ) := by
    ext i; simp
  rw[this, Finset.sup_insert]; simp
  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
  rw[this] }
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) → α
⊢ f 0 ⊔ (ofFn fun i => f i.succ).sup = Finset.univ.sup f
no goals