no goals
α : Type u_1
β : Type ?u.92502
γ : Type ?u.92505
ι : Sort u_2
ι' : Sort u_3
ι₂ : Sort ?u.92514
κ : ι → Sort ?u.92519
κ₁ : ι → Sort ?u.92524
κ₂ : ι → Sort ?u.92529
κ' : ι' → Sort ?u.92534
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 [iInter_and, @iInter_comm _ ι]