∀ {X Y U V : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (f' : U ⟶ V) (iU : U ⟶ X) (iV : V ⟶ Y)
  [inst : AlgebraicGeometry.IsOpenImmersion iV] [AlgebraicGeometry.QuasiCompact f],
  CategoryTheory.IsPullback f' iU iV f →
    ∀ (W : ↑V.affineOpens),
      (AlgebraicGeometry.Scheme.Hom.ker f').ideal W =
        Ideal.comap (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appIso iV ↑W).inv)
          ((AlgebraicGeometry.Scheme.Hom.ker f).ideal ⟨(AlgebraicGeometry.Scheme.Hom.opensFunctor iV).obj ↑W, ⋯⟩)