no goals
α : Type u_1
β : Type u_2
β₂ : Type ?u.212863
γ : Type ?u.212866
ι : Sort u_3
ι' : Sort ?u.212872
κ : ι → Sort ?u.212877
κ' : ι' → Sort ?u.212882
inst✝¹ : SupSet α
inst✝ : SupSet β
f : ι → α × β
⊢ swap (iSup f) = ⨆ (i : ι), swap (f i)
simp_rw [iSup, swap_sSup, ←range_comp, Function.comp]