no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.79430
ι : Sort x
f✝ g : Filter α
s t : Set α
S : Set (Set α)
f : Filter α
⊢ f ≤ generate S ↔ f ≤ ⨅ (s : Set α) (_ : s ∈ S), 𝓟 s
simp [le_generate_iff, le_principal_iff, subset_def]