∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] (f : NumberField.mixedEmbedding.mixedSpace K → E),
  ∫ (x : NumberField.mixedEmbedding.polarSpace K) in (NumberField.mixedEmbedding.polarSpaceCoord K).target,
      (∏ w, x.1 ↑w) • f (↑(NumberField.mixedEmbedding.polarSpaceCoord K).symm x) =
    ∫ (x : NumberField.mixedEmbedding.mixedSpace K), f x