no goals
α : Type u_1
β : Type ?u.5868
γ : Type ?u.5871
inst✝ : ConditionallyCompleteLattice α
s✝ t : Set α
a b : α
s : Finset α
hs : Finset.Nonempty s
⊢ sup' s hs id = sSup ↑s
rw [hs.sup'_eq_cSup_image, Set.image_id]