∀ {K : Type u_1} [inst : Field K] (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.normAtAllPlaces
      (NumberField.mixedEmbedding.mixedSpaceOfRealSpace (NumberField.mixedEmbedding.normAtAllPlaces x)) =
    NumberField.mixedEmbedding.normAtAllPlaces x