∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f]
  (U : { U // ↑U ≤ AlgebraicGeometry.Scheme.Hom.opensRange f }),
  AlgebraicGeometry.IsAffineOpen
    ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj ↑⟨(TopologicalSpace.Opens.map f.base).obj ↑↑U, ⋯⟩)