no goals
α : Type u_1
β : Type ?u.89841
γ : Type ?u.89844
ι : Sort u_2
ι' : Sort u_3
ι₂ : Sort ?u.89853
κ : ι → Sort ?u.89858
κ₁ : ι → Sort ?u.89863
κ₂ : ι → Sort ?u.89868
κ' : ι' → Sort ?u.89873
p : ι' → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p y ∧ q x y → Set α
⊢ (⋃ (x : ι) (y : ι') (h : p y ∧ q x y), s x y h) = ⋃ (y : ι') (hy : p y) (x : ι) (hx : q x y), s x y (_ : p y ∧ q x y)
simp only [iUnion_and, @iUnion_comm _ ι]