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