no goals
α : Type u_1
β : Type ?u.167312
γ : Type ?u.167315
ι : Sort ?u.167318
ι' : Sort ?u.167321
ι₂ : Sort ?u.167324
κ : ι → Sort ?u.167329
κ₁ : ι → Sort ?u.167334
κ₂ : ι → Sort ?u.167339
κ' : ι' → Sort ?u.167344
s : Set (Set α)
⊢ ⋃₀ s = ⋃ (i : ↑s), ↑i
simp only [← sUnion_range, Subtype.range_coe]