α : Type u_2
β : Type u_1
γ : Type ?u.18234
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ Prod.swap '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t
α : Type u_2
β : Type u_1
γ : Type ?u.18234
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ ↑(image Prod.swap (t ×ˢ s)) = ↑(s ×ˢ t)
push_cast
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.18234
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ Prod.swap '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t
exact Set.image_swap_prod _ _