no goals
ι : Type u_1
ι' : Type ?u.12466
α : ι → Type u_2
β : ι → Type ?u.12476
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
inst✝ : DecidablePred fun x => x ∈ s
⊢ Sigma.mk i ⁻¹' Set.Sigma s t = if i ∈ s then t i else ∅
split_ifs <;> simp [*]