no goals
ι : Type u_2
α : ι → Type u_1
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
I : Set ι
⊢ NeBot (pi f ⊓ 𝓟 (Set.pi I s)) ↔ ∀ (i : ι), i ∈ I → NeBot (f i ⊓ 𝓟 (s i))
simp [neBot_iff]