∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : K)
  (i : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)),
  ((NumberField.canonicalEmbedding.latticeBasis K).repr ((NumberField.canonicalEmbedding K) x)) i =
    ↑(((NumberField.integralBasis K).repr x) i)