no goals
ι : Type u_1
α : ι → Type u_2
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ Filter.coprodᵢ f = ⊥ ↔ (∃ i, IsEmpty (α i)) ∨ f = ⊥
simpa only [not_neBot, not_and_or, funext_iff, not_forall, not_exists, not_nonempty_iff]
  using coprodᵢ_neBot_iff'.not