no goals
α : Type u_1
β : Type u_2
γ : Type ?u.60908
δ : Type ?u.60911
ι : Sort ?u.60914
f : Filter α
g : Filter β
⊢ NeBot (Filter.coprod f g) ↔ NeBot f ∧ Nonempty β ∨ Nonempty α ∧ NeBot g
simp [Filter.coprod]