∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} (r : ↑(Y.presheaf.obj (Opposite.op U))),
  (TopologicalSpace.Opens.map f.base).obj (Y.basicOpen r) =
    X.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U)) r)