no goals
α✝ : Type ?u.65740
β✝ : Type ?u.65743
γ : Type ?u.65746
δ : Type ?u.65749
ι✝ : Sort ?u.65752
f : Filter α✝
g : Filter β✝
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
b : β
i : ι
⊢ Filter.coprod (map (fun x => b) (𝓟 {a})) (map id (𝓟 {i})) = 𝓟 ({b} ×ˢ univ ∪ univ ×ˢ {i})
simp only [map_principal, Filter.coprod, comap_principal, sup_principal, image_singleton,
  image_id, prod_univ, univ_prod, id]