∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K)
  (w : NumberField.InfinitePlace K),
  ↑NumberField.mixedEmbedding.fundamentalCone.expMap x w = Real.exp ((↑w.mult)⁻¹ * x w)