no goals
α : Type u_1
β : Type ?u.122213
γ : Type ?u.122216
ι : Sort ?u.122219
ι' : Sort ?u.122222
ι₂ : Sort ?u.122225
κ : ι → Sort ?u.122230
κ₁ : ι → Sort ?u.122235
κ₂ : ι → Sort ?u.122240
κ' : ι' → Sort ?u.122245
S : Set (Set α)
⊢ Set.Nonempty (⋃₀ S) ↔ ∃ s, s ∈ S ∧ Set.Nonempty s
simp [nonempty_iff_ne_empty]