no goals
α : Type ?u.42954
β : Type ?u.42957
γ : Type u_1
ι : Sort u_2
ι' : Sort ?u.42966
ι₂ : Sort ?u.42969
κ : ι → Sort u_3
κ₁ : ι → Sort ?u.42979
κ₂ : ι → Sort ?u.42984
κ' : ι' → Sort ?u.42989
x : γ
s : (i : ι) → κ i → Set γ
⊢ (x ∈ ⋂ (i : ι) (j : κ i), s i j) ↔ ∀ (i : ι) (j : κ i), x ∈ s i j
simp_rw [mem_iInter]