no goals
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.153466
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ : ι
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
⊢ pi univ (update (fun j => univ) i s) = eval i ⁻¹' s
rw [univ_pi_update i (fun j => (univ : Set (α j))) s fun j t => t, pi_univ, inter_univ, preimage]