no goals
α : Type u_1
β : Type u_2
γ : Type ?u.45737
ι : Sort ?u.45740
f✝ f : Filter α
g : Filter β
⊢ f ×ˢ g = Filter.lift f fun s => Filter.lift' g fun t => s ×ˢ t
simpa only [Filter.lift', Filter.lift, (f.basis_sets.prod g.basis_sets).eq_biInf,
  iInf_prod, iInf_and] using iInf_congr fun i => iInf_comm