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