-- 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
x : (↑(↑(Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯).toPresheafedSpace : TopCat) : Type u_1)
⊢ Eq (α :=
    Z.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 f.base g.base) ⋯) : TopCat))
                (PresheafedSpace.Hom.base
                    (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom ≫ f.toHom) :
                  (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⟶ (↑Z.toPresheafedSpace : TopCat)) :
              C((↑(↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) : Type u_1),
                (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))) :
            (a : (↑(↑(Y.restrict ⋯) : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
          x) ⟶
      (Y.restrict (U := pullback f.base g.base) ⋯).presheaf.stalk x)
    (PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom ≫ f.toHom) x :
      Z.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 f.base g.base) ⋯) : TopCat))
                  (PresheafedSpace.Hom.base
                      (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom ≫ f.toHom) :
                    (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⟶ (↑Z.toPresheafedSpace : TopCat)) :
                C((↑(↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) : Type u_1),
                  (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))) :
              (a : (↑(↑(Y.restrict ⋯) : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
            x) ⟶
        (Y.restrict (U := pullback f.base g.base) ⋯).presheaf.stalk x)
    (CategoryStruct.comp (Y :=
        Z.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 f.base g.base) ⋯) : TopCat))
                (PresheafedSpace.Hom.base (Y.ofRestrict ⋯ ≫ g.toHom)) :
              (a : (↑(↑(Y.restrict ⋯) : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
            x))
        (eqToHom ⋯) (PresheafedSpace.Hom.stalkMap (Y.ofRestrict ⋯ ≫ g.toHom) x) :
      Z.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 f.base g.base) ⋯) : TopCat))
                  (PresheafedSpace.Hom.base
                      (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom ≫ f.toHom) :
                    (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⟶ (↑Z.toPresheafedSpace : TopCat)) :
                C((↑(↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) : Type u_1),
                  (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))) :
              (a : (↑(↑(Y.restrict ⋯) : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
            x) ⟶
        (Y.restrict (U := pullback f.base g.base) ⋯).presheaf.stalk x)

Tactic:
have := PresheafedSpace.stalkMap.congr_hom _ _
        (PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition f.1 g.1) x