∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (k : K),
  ∀ᶠ (i : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite,
    (fun i => ↑k) i ∈ (fun v => ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) i