∀ {α : Type u_1} (motive : (x x_1 : UniformSpace.Core α) → x.uniformity = x_1.uniformity → Prop)
  (x x_1 : UniformSpace.Core α) (x_2 : x.uniformity = x_1.uniformity),
  (∀ (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)
      (refl_1 : Filter.principal SetRel.id ≤ uniformity) (symm_1 : Filter.Tendsto Prod.swap uniformity uniformity)
      (comp_1 : (uniformity.lift' fun s => SetRel.comp s s) ≤ uniformity),
      motive { uniformity := uniformity, refl := refl, symm := symm, comp := comp }
        { uniformity := uniformity, refl := refl_1, symm := symm_1, comp := comp_1 } ⋯) →
    motive x x_1 x_2