no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.20903
ι : Sort ?u.20906
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
h : Filter γ
⊢ map (↑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
simp_rw [map_equiv_symm, SProd.sprod, Filter.prod, comap_inf, comap_comap, inf_assoc,
  Function.comp, Equiv.prodAssoc_apply]