∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Algebra R ℚ] [inst_2 : IsIntegralClosure R ℤ ℚ]
  [inst_3 : IsDedekindDomain R] (p : Nat.Primes),
  (fun v => ⟨Rat.HeightOneSpectrum.natGenerator v, ⋯⟩)
      ((fun p =>
          have h := ⋯;
          IsDedekindDomain.HeightOneSpectrum.ofPrime h)
        p) =
    p