no goals
α : Type u_1
β : Type u_2
γ : Type ?u.28728
δ : Type ?u.28731
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝ : DecidablePred fun x => x ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = if a ∈ s then t else ∅
split_ifs with h <;> simp [h]