no goals
α : Type u_3
β : Type u_1
β₂ : Type ?u.165662
γ : Type u_2
ι : Sort ?u.165668
ι' : Sort ?u.165671
κ : ι → Sort ?u.165676
κ' : ι' → Sort ?u.165681
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : β × γ → α
c : α
⊢ (⨆ (x : β × γ), f x) ≤ c ↔ (⨆ (i : β) (j : γ), f (i, j)) ≤ c
simp only [iSup_le_iff, Prod.forall]