no goals
α : Type u
β : Type v
X : Type ?u.13
inst✝ : LinearOrder β
U : Filter (α × α)
z : β
D : α → α → β
H : ∀ (s : Set (α × α)), s ∈ U ↔ ∃ ε, ε > z ∧ ∀ {a b : α}, D a b < ε → (a, b) ∈ s
s : Set (α × α)
⊢ s ∈ U ↔ ∃ i, i > z ∧ {p | D p.fst p.snd < i} ⊆ s
simp only [H, subset_def, Prod.forall, mem_setOf]