no goals
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
p : ι → Prop
s : ι → Set (α × α)
h : HasBasis (𝓤 α) p s
f : Filter α
⊢ (∀ (i' : ι), p i' → ∃ i, i ∈ f ∧ id i ×ˢ id i ⊆ s i') ↔
    ∀ (i : ι), p i → ∃ t, t ∈ f ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (x, y) ∈ s i
simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, id, ball_mem_comm]