∀ {α : Type u} [toTopologicalSpace : TopologicalSpace α] [toTopologicalSpace_1 : TopologicalSpace α]
  (e_toTopologicalSpace : toTopologicalSpace = toTopologicalSpace_1) (uniformity uniformity_1 : Filter (α × α))
  (e_uniformity : uniformity = uniformity_1) (symm : Filter.Tendsto Prod.swap uniformity uniformity)
  (comp : (uniformity.lift' fun s => SetRel.comp s s) ≤ uniformity)
  (nhds_eq_comap_uniformity : ∀ (x : α), nhds x = Filter.comap (Prod.mk x) uniformity),
  { toTopologicalSpace := toTopologicalSpace, uniformity := uniformity, symm := symm, comp := comp,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity } =
    { toTopologicalSpace := toTopologicalSpace_1, uniformity := uniformity_1, symm := ⋯, comp := ⋯,
      nhds_eq_comap_uniformity := ⋯ }