no goals
α : Type u_1
β : Type ?u.167139
γ : Type ?u.167142
ι : Sort ?u.167145
ι' : Sort ?u.167148
ι₂ : Sort ?u.167151
κ : ι → Sort ?u.167156
κ₁ : ι → Sort ?u.167161
κ₂ : ι → Sort ?u.167166
κ' : ι' → Sort ?u.167171
s : Set (Set α)
⊢ ⋂₀ s = ⋂ (i : Set α) (_ : i ∈ s), i
rw [← sInter_image, image_id']