no goals
α : Type u_2
β : Type u_1
γ : Type ?u.43728
δ : Type ?u.43731
ι : Sort ?u.43734
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
a : α
f : Filter β
⊢ pure a ×ˢ f = map (Prod.mk a) f
rw [prod_eq, map_pure, pure_seq_eq_map]