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