no goals
F : Type ?u.291052
α : Type u_2
β : Type u_1
γ : Type ?u.291061
ι : Type ?u.291064
κ : Type ?u.291067
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
h : Finset.Nonempty s
f : β → α
⊢ ↑(sup s f) = sup s (WithBot.some ∘ f)
simp only [← sup'_eq_sup h, coe_sup' h]