no goals
α : Type u_1
β : Type ?u.25627
γ : Type ?u.25630
ι : Sort u_2
ι' : Sort u_3
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
hl' : HasBasis l' p' s'
⊢ l ≤ l' ↔ ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
simp only [hl'.ge_iff, hl.mem_iff]