no goals
α : Type u_1
β : Type u_2
γ : Type ?u.229496
ι : Sort ?u.229499
ι' : Sort ?u.229502
ι₂ : Sort ?u.229505
κ : ι → Sort ?u.229510
κ₁ : ι → Sort ?u.229515
κ₂ : ι → Sort ?u.229520
κ' : ι' → Sort ?u.229525
s : Set α
C : Set (Set β)
⊢ s ×ˢ ⋃₀ C = ⋃₀ ((fun t => s ×ˢ t) '' C)
simp_rw [sUnion_eq_biUnion, biUnion_image, prod_iUnion₂]