no goals
α : Type u_1
β : Type ?u.9944
γ : Type ?u.9947
ι : Sort ?u.9950
ι' : Sort ?u.9953
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s : Set (Set α)
U : Set α
⊢ U ∈ generate s ↔ ∃ i, (Set.Finite i ∧ i ⊆ s) ∧ ⋂₀ i ⊆ U
simp only [mem_generate_iff, exists_prop, and_assoc, and_left_comm]