∀ {X Y Z : AlgebraicGeometry.Scheme} (f g : X ⟶ Y) (i : Y ⟶ Z) [AlgebraicGeometry.IsSeparated i]
  [AlgebraicGeometry.IsReduced X] (S : Set ↥X),
  Dense S →
    (∀ x ∈ S,
        CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) f =
          CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) g) →
      CategoryTheory.CategoryStruct.comp f i = CategoryTheory.CategoryStruct.comp g i → f = g