no goals
α : Type u_1
β : Type ?u.128133
γ : Type ?u.128136
ι : Sort u_2
ι' : Sort ?u.128142
ι₂ : Sort ?u.128145
κ : ι → Sort u_3
κ₁ : ι → Sort ?u.128155
κ₂ : ι → Sort ?u.128160
κ' : ι' → Sort ?u.128165
s : (i : ι) → κ i → Set α
⊢ (⋃ (i : ι) (j : κ i), s i j) = univ ↔ ∀ (a : α), ∃ i j, a ∈ s i j
simp only [iUnion_eq_univ_iff, mem_iUnion]