∀ {A : Type} {inst : MetricSpace A} {Space : Type} {metric : MetricSpace Space} {embed : A → Space}
  {isom : Isometry embed} {Space_1 : Type} {metric_1 : MetricSpace Space_1} {embed_1 : A → Space_1}
  {isom_1 : Isometry embed_1},
  { Space := Space, metric := metric, embed := embed, isom := isom } =
      { Space := Space_1, metric := metric_1, embed := embed_1, isom := isom_1 } →
    Space = Space_1 ∧ metric ≍ metric_1 ∧ embed ≍ embed_1