no goals
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.3707
δ : Type ?u.3710
ι : Sort u_4
κ : ι → Sort ?u.3718
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : sSupHomClass F α β
f : F
g : ι → α
⊢ ↑f (⨆ (i : ι), g i) = ⨆ (i : ι), ↑f (g i)
simp [iSup, ← Set.range_comp, Function.comp]