no goals
α : Type u_1
β : Type ?u.61688
γ : Type ?u.61691
ι : Sort u_2
ι' : Sort ?u.61697
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l (fun x => True) s
⊢ l = ⨅ (i : ι), 𝓟 (s i)
simpa only [iInf_true] using h.eq_biInf