∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (self : AlgebraicGeometry.ValuativeCommSq f),
  CategoryTheory.CommSq self.i₁ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap self.R self.K))) f self.i₂