no goals
α : Type u_1
β : Type ?u.179429
γ : Type ?u.179432
ι : Sort u_2
ι' : Sort ?u.179438
ι₂ : Sort ?u.179441
κ : ι → Sort ?u.179446
κ₁ : ι → Sort ?u.179451
κ₂ : ι → Sort ?u.179456
κ' : ι' → Sort ?u.179461
s : ι → Set (Set α)
⊢ (⋂₀ ⋃ (i : ι), s i) = ⋂ (i : ι), ⋂₀ s i
simp only [sInter_eq_biInter, biInter_iUnion]