no goals
α : Type u_1
β : Type u_2
γ : Type ?u.28906
s s' : Finset α
t t' : Finset β
a : α
b : β
p : α → Prop
inst✝ : DecidablePred p
⊢ filter (fun x => p x.fst) (s ×ˢ t) = filter p s ×ˢ t
simpa using filter_product p fun _ => true