α : Type u_1
β : Type u_2
γ : Type ?u.17685
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
⊢ (fun a => ↑{ toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } a) '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t
α : Type u_1
β : Type u_2
γ : Type ?u.17685
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
⊢ ↑(map { toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } (t ×ˢ s)) = ↑(s ×ˢ t)
push_cast
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.17685
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
⊢ (fun a => ↑{ toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } a) '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t
exact Set.image_swap_prod _ _