{X Y : AlgebraicGeometry.Scheme} →
  {f : X ⟶ Y} →
    (R : Type u) →
      [commRing : CommRing R] →
        [domain : IsDomain R] →
          [valuationRing : ValuationRing R] →
            (K : Type u) →
              [field : Field K] →
                [algebra : Algebra R K] →
                  [isFractionRing : IsFractionRing R K] →
                    (i₁ : AlgebraicGeometry.Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing } ⟶ X) →
                      (i₂ : AlgebraicGeometry.Spec { carrier := R, commRing := commRing } ⟶ Y) →
                        CategoryTheory.CommSq i₁ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))) f
                            i₂ →
                          AlgebraicGeometry.ValuativeCommSq f