no goals
F : Type ?u.450915
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.450927
κ : Type ?u.450930
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
f : γ → α
g : α → β
s : Finset γ
⊢ (⨆ (x : α) (_ : x ∈ image f s), g x) = ⨆ (y : γ) (_ : y ∈ s), g (f y)
rw [← iSup_coe, coe_image, iSup_image, iSup_coe]