no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.29388
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝ : DecidablePred fun x => x ∈ t
f : γ → α
⊢ (fun a => (f a, b)) ⁻¹' s ×ˢ t = if b ∈ t then f ⁻¹' s else ∅
rw [← mk_preimage_prod_left_eq_if, prod_preimage_left, preimage_preimage]