no goals
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.114693
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
x : (i : ι) → α i
⊢ (x ∈ pi s fun i => t i ∩ t₁ i) ↔ x ∈ pi s t ∩ pi s t₁
simp only [forall_and, mem_pi, mem_inter_iff]