no goals
α : Type u_1
β : Type u_2
γ : Type ?u.228853
ι : Sort u_3
ι' : Sort ?u.228859
ι₂ : Sort ?u.228862
κ : ι → Sort u_4
κ₁ : ι → Sort ?u.228872
κ₂ : ι → Sort ?u.228877
κ' : ι' → Sort ?u.228882
s : Set α
t : (i : ι) → κ i → Set β
⊢ (s ×ˢ ⋃ (i : ι) (j : κ i), t i j) = ⋃ (i : ι) (j : κ i), s ×ˢ t i j
simp_rw [prod_iUnion]