∀ {K : Type u_1} [inst : Field K] {X : AlgebraicGeometry.Scheme}
  {f₁ f₂ : (x : ↥X) × (X.residueField x ⟶ { carrier := K, commRing := Field.toEuclideanDomain.toCommRing })},
  f₁ = f₂ ↔
    ∃ (e : f₁.fst = f₂.fst),
      f₁.snd = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr e).hom f₂.snd