∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X),
  CategoryTheory.inv (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f U) =
    CategoryTheory.CategoryStruct.comp
      (f.c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj U)))
      (X.presheaf.map (CategoryTheory.eqToHom ⋯))