no goals
α : Type u_1
α' : Type ?u.19006
β : Type u_2
β' : Type ?u.19012
γ : Type ?u.19015
γ' : Type ?u.19018
δ : Type ?u.19021
δ' : Type ?u.19024
ε : Type ?u.19027
ε' : Type ?u.19030
m : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
f : Filter α
g : Filter β
⊢ map₂ Prod.mk f g = f ×ˢ g
simp only [← map_prod_eq_map₂, map_id']