simp[ih]
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
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 ⊔ Finset.univ.sup fun i => f i.succ) = Finset.univ.sup f