no goals
α : Type u_2
β : Type u_1
γ : Type ?u.153217
ι : Sort ?u.153220
ι' : Sort ?u.153223
ι₂ : Sort ?u.153226
κ : ι → Sort ?u.153231
κ₁ : ι → Sort ?u.153236
κ₂ : ι → Sort ?u.153241
κ' : ι' → Sort ?u.153246
s : α → Set β
⊢ (⋃ (i : α), s i) = range fun a => ↑a.snd
simp [Set.ext_iff]