{X Y Z : AlgebraicGeometry.LocallyRingedSpace} →
  (f : X ⟶ Z) →
    (g : Y ⟶ Z) →
      [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] →
        Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆
            Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) →
          (Y ⟶ X)