no goals
α : Type u_2
β : Type u_1
β₂ : Type ?u.111484
γ : Type ?u.111487
ι : Sort ?u.111490
ι' : Sort ?u.111493
κ : ι → Sort ?u.111498
κ' : ι' → Sort ?u.111503
inst✝ : CompleteLattice α
f✝ g s✝ t : ι → α
a b : α
s : Set β
f : β → α
⊢ sSup (f '' s) = ⨆ (a : β) (_ : a ∈ s), f a
rw [← iSup_subtype'', sSup_image']