no goals
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
⊢ ↑(prodAssoc α β γ).symm '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u
simpa only [Equiv.image_eq_preimage] using prod_assoc_preimage