simp only [Set.mem_iUnion, exists_prop]
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
hx : x ∈ ⋃ j ∈ J, A j
⊢ x ∈ ⋃ i ∈ I, A i
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
hx : x ∈ ⋃ j ∈ J, A j
⊢ ∃ i ∈ I, x ∈ A i