{α : Type u} →
  [toDist : Dist α] →
    (∀ (x : α), dist x x = 0) →
      (∀ (x y : α), dist x y = dist y x) →
        (∀ (x y z : α), dist x z ≤ dist x y + dist y z) →
          (edist : α → α → ENNReal) →
            autoParam (∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)) PseudoMetricSpace.edist_dist._autoParam →
              (toUniformSpace : UniformSpace α) →
                autoParam (uniformity α = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | dist p.1 p.2 < ε})
                    PseudoMetricSpace.uniformity_dist._autoParam →
                  (toBornology : Bornology α) →
                    autoParam ((Bornology.cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C})
                        PseudoMetricSpace.cobounded_sets._autoParam →
                      PseudoMetricSpace α