no goals
α : Type u_1
β : Type u_2
γ : Type ?u.42847
δ : Type ?u.42850
ι : Sort ?u.42853
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
g₁ g₂ : Filter β
⊢ f ×ˢ (g₁ ⊓ g₂) = f ×ˢ g₁ ⊓ f ×ˢ g₂
rw [prod_inf_prod, inf_idem]