no goals
α : Type u_1
β : Type u_2
γ : Type ?u.30722
δ : Type ?u.30725
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
s : Set α
t : Set β
⊢ Prod.swap '' s ×ˢ t = t ×ˢ s
rw [image_swap_eq_preimage_swap, preimage_swap_prod]