no goals
ι : Type u_1
α : ι → Type u_3
β✝ : ι → Type ?u.152906
s s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i✝ : ι
inst✝ : DecidableEq ι
β : ι → Type u_2
i : ι
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (pi univ fun j => t j (update f i a j)) = {x | x i ∈ t i a} ∩ pi ({i}ᶜ) fun j => t j (f j)
rw [compl_eq_univ_diff, ← pi_update_of_mem (mem_univ _)]