∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace)
  {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_1 : CategoryTheory.ConcreteCategory C F] (x : carrier (X.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom
        (f.hom.c.app (Opposite.op ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f).obj U))))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f U)) x) =
    (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.eqToHom ⋯))) x