no goals
α : Type ?u.42510
β : Type ?u.42513
γ : Type u_1
ι : Sort u_2
ι' : Sort ?u.42522
ι₂ : Sort ?u.42525
κ : ι → Sort u_3
κ₁ : ι → Sort ?u.42535
κ₂ : ι → Sort ?u.42540
κ' : ι' → Sort ?u.42545
x : γ
s : (i : ι) → κ i → Set γ
⊢ (x ∈ ⋃ (i : ι) (j : κ i), s i j) ↔ ∃ i j, x ∈ s i j
simp_rw [mem_iUnion]