no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.4517
ι : Sort ?u.4520
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : α → β × γ
b : Filter β
c : Filter γ
⊢ comap f (b ×ˢ c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
erw [comap_inf, Filter.comap_comap, Filter.comap_comap]