no goals
F : Type ?u.57927
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.57939
κ : Type ?u.57942
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β × γ → α
⊢ sup (s ×ˢ t) f = sup t fun i' => sup s fun i => f (i, i')
rw [sup_product_left, Finset.sup_comm]