no goals
α : Type u_1
β : Type ?u.127762
γ : Type ?u.127765
ι : Sort u_2
ι' : Sort ?u.127771
ι₂ : Sort ?u.127774
κ : ι → Sort ?u.127779
κ₁ : ι → Sort ?u.127784
κ₂ : ι → Sort ?u.127789
κ' : ι' → Sort ?u.127794
f : ι → Set α
⊢ (⋃ (i : ι), f i) = univ ↔ ∀ (x : α), ∃ i, x ∈ f i
simp only [eq_univ_iff_forall, mem_iUnion]