no goals
α : Type u_1
β : Type ?u.167787
γ : Type ?u.167790
ι : Sort ?u.167793
ι' : Sort ?u.167796
ι₂ : Sort ?u.167799
κ : ι → Sort ?u.167804
κ₁ : ι → Sort ?u.167809
κ₂ : ι → Sort ?u.167814
κ' : ι' → Sort ?u.167819
s : Set (Set α)
⊢ ⋂₀ s = ⋂ (i : ↑s), ↑i
simp only [← sInter_range, Subtype.range_coe]