no goals
α : Type u_1
β : Type ?u.60356
γ : Type ?u.60359
ι : Sort u_2
ι' : Sort ?u.60365
ι₂ : Sort ?u.60368
κ : ι → Sort u_3
κ₁ : ι → Sort ?u.60378
κ₂ : ι → Sort ?u.60383
κ' : ι' → Sort ?u.60388
s : Set α
t : (i : ι) → κ i → Set α
⊢ (s ⊆ ⋂ (i : ι) (j : κ i), t i j) ↔ ∀ (i : ι) (j : κ i), s ⊆ t i j
simp_rw [subset_iInter_iff]