no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.28964
ι : Sort ?u.28967
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : β → γ
F : Filter α
G : Filter β
⊢ F ×ˢ map f G = map (Prod.map id f) (F ×ˢ G)
rw [← prod_map_map_eq', map_id]