no goals
α : Type u_1
β : Type ?u.99755
γ : Type ?u.99758
ι : Sort ?u.99761
ι' : Sort ?u.99764
ι₂ : Sort ?u.99767
κ : ι → Sort ?u.99772
κ₁ : ι → Sort ?u.99777
κ₂ : ι → Sort ?u.99782
κ' : ι' → Sort ?u.99787
s : Set α
⊢ (⋃ (_ : Set.Nonempty s), s) = s
rw [iUnion_nonempty_index, biUnion_self]