∀ {P : AlgebraicGeometry.AffineTargetMorphismProperty},
  P.toProperty.RespectsIso →
    (∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y)
        (r : ↑(Y.presheaf.obj (Opposite.op ⊤))), P f → P (f ∣_ Y.basicOpen r)) →
      (∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y)
          (s : Finset ↑(Y.presheaf.obj (Opposite.op ⊤))),
          Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (f ∣_ Y.basicOpen ↑r)) → P f) →
        P.IsLocal