∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K)
  (w : { w // w.IsComplex }), ((NumberField.mixedEmbedding.stdBasis K).repr x) (Sum.inr (w, 0)) = (x.2 w).re