no goals
α : Type u_1
β : Type u_2
γ : Type ?u.257901
ι : Sort ?u.257904
ι' : Sort ?u.257907
ι₂ : Sort ?u.257910
κ : ι → Sort ?u.257915
κ₁ : ι → Sort ?u.257920
κ₂ : ι → Sort ?u.257925
κ' : ι' → Sort ?u.257930
f : α → β → γ
s : Set α
t : Set β
⊢ s ×ˢ t = ⋃ (b : β) (_ : b ∈ t), (fun a => (a, b)) '' s
rw [iUnion_image_right, image2_mk_eq_prod]