no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.93034
inst✝ : UniformSpace α
p : β → Prop
s : β → Set (α × α)
h : HasBasis (𝓤 α) p s
t : Set (α × α)
⊢ (∃ i, p i ∧ s i ⊆ t) ↔ ∃ i, p i ∧ ∀ (a b : α), (a, b) ∈ s i → (a, b) ∈ t
simp only [Prod.forall, subset_def]