∀ {α : Type u} (uniformity : Filter (α × α)) (refl : Filter.principal SetRel.id ≤ uniformity)
  (symm : Filter.Tendsto Prod.swap uniformity uniformity)
  (comp : (uniformity.lift' fun s => SetRel.comp s s) ≤ uniformity) (uniformity_1 : Filter (α × α))
  (refl_1 : Filter.principal SetRel.id ≤ uniformity_1) (symm_1 : Filter.Tendsto Prod.swap uniformity_1 uniformity_1)
  (comp_1 : (uniformity_1.lift' fun s => SetRel.comp s s) ≤ uniformity_1),
  ({ uniformity := uniformity, refl := refl, symm := symm, comp := comp } =
      { uniformity := uniformity_1, refl := refl_1, symm := symm_1, comp := comp_1 }) =
    (uniformity = uniformity_1)