no goals
α : Type u_1
β : Type ?u.81842
γ : Type ?u.81845
ι : Sort u_2
ι' : Sort ?u.81851
ι₂ : Sort ?u.81854
κ : ι → Sort ?u.81859
κ₁ : ι → Sort ?u.81864
κ₂ : ι → Sort ?u.81869
κ' : ι' → Sort ?u.81874
s : ι → Set α
⊢ Set.Nonempty (⋃ (i : ι), s i) ↔ ∃ i, Set.Nonempty (s i)
simp [nonempty_iff_ne_empty]