∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↥(CategoryTheory.Limits.pullback f g)),
  (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).x = (CategoryTheory.Limits.pullback.fst f g) t