no goals
α : Type u_1
β : Type u_2
γ : Type ?u.169471
ι : Sort u_3
ι' : Sort ?u.169477
ι₂ : Sort ?u.169480
κ : ι → Sort ?u.169485
κ₁ : ι → Sort ?u.169490
κ₂ : ι → Sort ?u.169495
κ' : ι' → Sort ?u.169500
s : ι → Set α
t : α → Set β
⊢ (⋃ (x : α) (_ : x ∈ ⋃ (i : ι), s i), t x) = ⋃ (i : ι) (x : α) (_ : x ∈ s i), t x
simp [@iUnion_comm _ ι]