no goals
F : Type ?u.230811
α : Type u_1
β : Type u_2
γ : Type ?u.230820
ι : Type ?u.230823
κ : Type ?u.230826
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f : β → α
⊢ ↑(sup' s H f) = sup s (WithBot.some ∘ f)
rw [sup', WithBot.coe_unbot]