∀ {ι : Type u_1} {α : Type u_2} {κ : ι → Type u_3} [inst : (i : ι) → Fintype (κ i)] (s : Finset ι)
  (f : (i : ι) → κ i → Set α), ⋂ i ∈ s, ⋂ j, f i j = ⋂ ij ∈ s.sigma fun x => Finset.univ, f ij.fst ij.snd