no goals
α : Type u_1
β : Type u_2
γ : Type ?u.62155
δ : Type ?u.62158
ι : Sort ?u.62161
f : Filter α
g : Filter β
s : Set α
t : Set β
⊢ Filter.coprod (𝓟 s) (𝓟 t) = 𝓟 ((sᶜ ×ˢ tᶜ)ᶜ)
rw [Filter.coprod, comap_principal, comap_principal, sup_principal, Set.prod_eq, compl_inter,
  preimage_compl, preimage_compl, compl_compl, compl_compl]