∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ)
  {x : NumberField.mixedEmbedding.mixedSpace K},
  x ∈ NumberField.mixedEmbedding.idealLattice K I ↔ ∃ y ∈ ↑↑I, (NumberField.mixedEmbedding K) y = x