∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Algebra R ℚ] [inst_2 : IsIntegralClosure R ℤ ℚ]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R ℚ] (v : IsDedekindDomain.HeightOneSpectrum R)
  (x y : UniformSpace.Completion (WithVal (IsDedekindDomain.HeightOneSpectrum.valuation ℚ v))),
  ((UniformSpace.Completion.mapRingEquiv
              (WithVal.equivWithVal (IsDedekindDomain.HeightOneSpectrum.valuation ℚ v)
                (Rat.padicValuation ↑(Rat.HeightOneSpectrum.primesEquiv v)))
              ⋯ ⋯).trans
          Padic.withValRingEquiv).toFun
      (x + y) =
    ((UniformSpace.Completion.mapRingEquiv
                (WithVal.equivWithVal (IsDedekindDomain.HeightOneSpectrum.valuation ℚ v)
                  (Rat.padicValuation ↑(Rat.HeightOneSpectrum.primesEquiv v)))
                ⋯ ⋯).trans
            Padic.withValRingEquiv).toFun
        x +
      ((UniformSpace.Completion.mapRingEquiv
                (WithVal.equivWithVal (IsDedekindDomain.HeightOneSpectrum.valuation ℚ v)
                  (Rat.padicValuation ↑(Rat.HeightOneSpectrum.primesEquiv v)))
                ⋯ ⋯).trans
            Padic.withValRingEquiv).toFun
        y