no goals
α : Type u_3
β : Type u_1
β₂ : Type ?u.175570
γ : Type u_2
ι : Sort ?u.175576
ι' : Sort ?u.175579
κ : ι → Sort ?u.175584
κ' : ι' → Sort ?u.175589
inst✝ : CompleteLattice α
f✝ g s✝ t✝ : ι → α
a b : α
f : β → γ → α
s : Set β
t : Set γ
⊢ sSup (image2 f s t) = ⨆ (a : β) (_ : a ∈ s) (b : γ) (_ : b ∈ t), f a b
rw [← image_prod, sSup_image, biSup_prod]