no goals
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → ℕ → α
⊢ (⨆ (n : ℕ), f (unpair n).fst (unpair n).snd) = ⨆ (i : ℕ) (j : ℕ), f i j
rw [← (iSup_prod : (⨆ i : ℕ × ℕ, f i.1 i.2) = _), ← Nat.surjective_unpair.iSup_comp]