no goals
α : Type u_1
β : Type ?u.43930
γ : Type ?u.43933
ι : Sort u_2
ι' : Sort ?u.43939
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s'✝ : ι' → Set α
i' : ι'
hl : HasBasis l p s
s' t : Set α
⊢ t ∈ l ⊓ 𝓟 s' ↔ ∃ i, p i ∧ s i ∩ s' ⊆ t
simp only [mem_inf_principal, hl.mem_iff, subset_def, mem_setOf_eq, mem_inter_iff, and_imp]