∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace),
  (TopologicalSpace.Opens.map f.hom.base).op.obj
      (Opposite.op ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f).obj U)) =
    Opposite.op U