∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)),
  Ideal.absNorm v.asIdeal ≤ 1 → 0 < Ideal.absNorm v.asIdeal → Ideal.absNorm v.asIdeal = 1