∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  ↑(NumberField.mixedEmbedding.polarCoordReal K).symm ''
      (NumberField.mixedEmbedding.polarCoordReal K).target =ᵐ[MeasureTheory.volume]
    Set.univ