-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
prop :
  ∀ (x : (↑(↑(Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯).toPresheafedSpace : TopCat) : Type u_1)),
    IsLocalHom (R :=
      (↑(X.presheaf.stalk
            (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    TopCat.carrier) (X :=
                    (↑(Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯).toPresheafedSpace : TopCat))
                    (PresheafedSpace.Hom.base (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) :
                      (↑(Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯).toPresheafedSpace : TopCat) ⟶
                        (↑X.toPresheafedSpace : TopCat)) :
                  C((↑(↑(Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯).toPresheafedSpace : TopCat) :
                      Type u_1),
                    (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) :
                (a : (↑(↑(Y.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                  (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
              x)) :
        Type u_1))
      (S := (↑((Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯).presheaf.stalk x) : Type u_1)) (F :=
      (↑(X.presheaf.stalk
              (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                      TopCat.carrier) (X :=
                      (↑(Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯).toPresheafedSpace : TopCat))
                      (PresheafedSpace.Hom.base
                          (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) :
                        (↑(Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯).toPresheafedSpace : TopCat) ⟶
                          (↑X.toPresheafedSpace : TopCat)) :
                    C((↑(↑(Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯).toPresheafedSpace : TopCat) :
                        Type u_1),
                      (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) :
                  (a : (↑(↑(Y.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                    (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
                x)) :
          Type u_1) →+*
        (↑((Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯).presheaf.stalk x) : Type u_1))
      (CommRingCat.Hom.hom
          (PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) x) :
        (↑(X.presheaf.stalk
                (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                        TopCat.carrier) (X :=
                        (↑(Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯).toPresheafedSpace : TopCat))
                        (PresheafedSpace.Hom.base
                            (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) :
                          (↑(Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯).toPresheafedSpace : TopCat) ⟶
                            (↑X.toPresheafedSpace : TopCat)) :
                      C((↑(↑(Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯).toPresheafedSpace : TopCat) :
                          Type u_1),
                        (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) :
                    (a : (↑(↑(Y.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                      (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
                  x)) :
            Type u_1) →+*
          (↑((Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯).presheaf.stalk x) : Type u_1))
⊢ Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯ ⟶ X

Tactic:
use PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.1 g.1

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst