have := hu.coe_sort
α : Type u_1
ι : Type u_2
s : ι → Set α
u : Set ι
hu : u.Nonempty
t : Set α
⊢ t ∩ ⋂ i ∈ u, s i = ⋂ i ∈ u, t ∩ s i
α : Type u_1
ι : Type u_2
s : ι → Set α
u : Set ι
hu : u.Nonempty
t : Set α
this : Nonempty ↑u
⊢ t ∩ ⋂ i ∈ u, s i = ⋂ i ∈ u, t ∩ s i