no goals
α : Type u_1
β : Type ?u.44590
γ : Type ?u.44593
ι : Sort u_2
ι' : Sort ?u.44599
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s'✝ : ι' → Set α
i' : ι'
hl : HasBasis l p s
s' : Set α
⊢ HasBasis (𝓟 s' ⊓ l) p fun i => s' ∩ s i
simpa only [inf_comm, inter_comm] using hl.inf_principal s'