∀ {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) (g : ↥X → ↥Y) (h : ⇑f = g) (x : ↥X),
  IsLocalHom
    (CommRingCat.Hom.hom
      ({ base := TopCat.ofHom { toFun := g, continuous_toFun := ⋯ },
            c := CategoryTheory.CategoryStruct.comp f.c (TopCat.Presheaf.pushforwardEq ⋯ X.presheaf).hom }.stalkMap
        x))