no goals
α : Type u_1
β : Type u_2
γ : Type ?u.45152
δ : Type ?u.45155
ι : Sort ?u.45158
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
simp_rw [← empty_mem_iff_bot, mem_prod_iff, subset_empty_iff, prod_eq_empty_iff, ← exists_prop,
  Subtype.exists', exists_or, exists_const, Subtype.exists, exists_prop, exists_eq_right]