∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens)
  (x : ↑(Y.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.IsOpenImmersion.ΓIso f U).hom)
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U)) x) =
    (CategoryTheory.ConcreteCategory.hom (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op)) x