no goals
α : Type u_1
β : Type u_2
γ : Type ?u.232963
ι : Sort ?u.232966
ι' : Sort ?u.232969
ι₂ : Sort ?u.232972
κ : ι → Sort ?u.232977
κ₁ : ι → Sort ?u.232982
κ₂ : ι → Sort ?u.232987
κ' : ι' → Sort ?u.232992
C : Set (Set α)
t : Set β
⊢ ⋃₀ C ×ˢ t = ⋃₀ ((fun s => s ×ˢ t) '' C)
simp only [sUnion_eq_biUnion, iUnion₂_prod_const, biUnion_image]