no goals
α : Type u_1
β : Type u_2
β₂ : Type ?u.211513
γ : Type ?u.211516
ι : Sort u_3
ι' : Sort ?u.211522
κ : ι → Sort ?u.211527
κ' : ι' → Sort ?u.211532
inst✝¹ : InfSet α
inst✝ : InfSet β
f : ι → α × β
⊢ swap (iInf f) = ⨅ (i : ι), swap (f i)
simp_rw [iInf, swap_sInf, ←range_comp, Function.comp]