∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.integerSet K =
    NumberField.mixedEmbedding.fundamentalCone K ∩ ↑(NumberField.mixedEmbedding.integerLattice K)