no goals
α : Type u_1
β : Type u_2
γ : Type ?u.299540
ι : Sort ?u.299543
ι' : Sort ?u.299546
ι₂ : Sort ?u.299549
κ : ι → Sort ?u.299554
κ₁ : ι → Sort ?u.299559
κ₂ : ι → Sort ?u.299564
κ' : ι' → Sort ?u.299569
t : α → Set β
b : β
hb : b ∈ ⋃ (i : α), t i
⊢ ∃ a, b ∈ t a
simpa using hb