no goals
α : Type u_1
β : Type u_2
γ : Type ?u.41525
δ : Type ?u.41528
ι : Sort ?u.41531
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
⊢ f₁ ×ˢ g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ⊓ f₂) ×ˢ (g₁ ⊓ g₂)
simp only [SProd.sprod, Filter.prod, comap_inf, inf_comm, inf_assoc, inf_left_comm]