no goals
α : Type u_1
β : Type ?u.42785
γ : Type ?u.42788
ι : Sort u_2
ι' : Sort ?u.42794
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
t u : Set α
⊢ u ∈ l ⊔ 𝓟 t ↔ ∃ i, p i ∧ s i ∪ t ⊆ u
simp only [(hl.sup' (hasBasis_principal t)).mem_iff, PProd.exists, exists_prop, and_true_iff,
  Unique.exists_iff]