no goals
α : Type u_1
β : Type u_2
γ : Type ?u.232320
ι : Sort u_3
ι' : Sort ?u.232326
ι₂ : Sort ?u.232329
κ : ι → Sort u_4
κ₁ : ι → Sort ?u.232339
κ₂ : ι → Sort ?u.232344
κ' : ι' → Sort ?u.232349
s : (i : ι) → κ i → Set α
t : Set β
⊢ (⋃ (i : ι) (j : κ i), s i j) ×ˢ t = ⋃ (i : ι) (j : κ i), s i j ×ˢ t
simp_rw [iUnion_prod_const]