no goals
α : Type u_1
β : Type ?u.21459
γ : Type ?u.21462
ι : Sort ?u.21465
ι' : Sort ?u.21468
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s : Set (Set α)
⊢ (∀ {i : Set (Set α)}, Set.Finite i ∧ i ⊆ s → Set.Nonempty (⋂₀ i)) ↔
    ∀ (t : Set (Set α)), t ⊆ s → Set.Finite t → Set.Nonempty (⋂₀ t)
simp only [← and_imp, and_comm]