∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))))
  (a : ↑(NumberField.mixedEmbedding.fundamentalCone.idealSet K J)),
  ↑(NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet
        (NumberField.mixedEmbedding.fundamentalCone.idealSetMap K J a)) ∈
    ↑↑J