∀ {K : Type u_1} [inst : Field K] {A : Set (NumberField.mixedEmbedding.mixedSpace K)},
  NumberField.mixedEmbedding.normAtComplexPlaces ⁻¹' (NumberField.mixedEmbedding.normAtComplexPlaces '' A) = A →
    NumberField.mixedEmbedding.normAtComplexPlaces '' A =
      ⇑NumberField.mixedEmbedding.mixedSpaceOfRealSpace ⁻¹' A ∩
        Set.univ.pi fun w => if w.IsReal then Set.univ else Set.Ici 0