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