∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Algebra R ℚ] [inst_3 : IsFractionRing R ℚ]
  {𝔭 : IsDedekindDomain.HeightOneSpectrum R} {x : ℚ},
  ((IsDedekindDomain.HeightOneSpectrum.valuation ℚ 𝔭) x ≤ 1) = (↑x.den ∉ 𝔭.asIdeal)