no goals
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.5694
δ : Type ?u.5697
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : sSupHomClass F α β
f : F
g : (i : ι) → κ i → α
⊢ ↑f (⨆ (i : ι) (j : κ i), g i j) = ⨆ (i : ι) (j : κ i), ↑f (g i j)
simp_rw [map_iSup]