-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
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)
this :
  Eq (α :=
    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 f.base g.base) ⋯) : TopCat))
                (PresheafedSpace.Hom.base (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) :
                  (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⟶ (↑X.toPresheafedSpace : TopCat)) :
              C((↑(↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) : Type u_1),
                (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) :
            (a : (↑(↑(Y.restrict ⋯) : TopCat) : Type u_1)) → (↑(↑X.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) 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 f.base g.base) ⋯) : TopCat))
                  (PresheafedSpace.Hom.base (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) :
                    (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⟶ (↑X.toPresheafedSpace : TopCat)) :
                C((↑(↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) : Type u_1),
                  (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) :
              (a : (↑(↑(Y.restrict ⋯) : TopCat) : Type u_1)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
            x) ⟶
        (Y.restrict (U := pullback f.base g.base) ⋯).presheaf.stalk x)
    (inv
          (f.stalkMap
            (((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) :
                      (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⟶ (↑X.toPresheafedSpace : TopCat)) :
                  C((↑(↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) : Type u_1),
                    (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) :
                (a : (↑(↑(Y.restrict ⋯) : TopCat) : Type u_1)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
              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 ⋯)
          (g.stalkMap
              ((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 ⋯)) :
                  (a : (↑(↑(Y.restrict ⋯) : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
                x) ≫
            PresheafedSpace.Hom.stalkMap (Y.ofRestrict ⋯) 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 f.base g.base) ⋯) : TopCat))
                  (PresheafedSpace.Hom.base (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) :
                    (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⟶ (↑X.toPresheafedSpace : TopCat)) :
                C((↑(↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) : Type u_1),
                  (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) :
              (a : (↑(↑(Y.restrict ⋯) : TopCat) : Type u_1)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
            x) ⟶
        (Y.restrict (U := pullback f.base g.base) ⋯).presheaf.stalk x)
⊢ 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))
have prop : 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) sorry).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) :
                  (↑(Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) sorry).toPresheafedSpace : TopCat) ⟶
                    (↑X.toPresheafedSpace : TopCat)) :
              C((↑(↑(Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) sorry).toPresheafedSpace : TopCat) :
                  Type u_1),
                (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) :
            (a : (↑(↑(Y.restrict sorry).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) sorry).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) sorry).toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) :
                    (↑(Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) sorry).toPresheafedSpace : TopCat) ⟶
                      (↑X.toPresheafedSpace : TopCat)) :
                C((↑(↑(Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) sorry).toPresheafedSpace : TopCat) :
                    Type u_1),
                  (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) :
              (a : (↑(↑(Y.restrict sorry).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) sorry).presheaf.stalk x) : Type u_1))
  (CommRingCat.Hom.hom
    (inv
        (f.stalkMap
          (((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) sorry) : TopCat))
                  (PresheafedSpace.Hom.base (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) :
                    (↑(Y.restrict (U := pullback f.base g.base) sorry) : TopCat) ⟶ (↑X.toPresheafedSpace : TopCat)) :
                C((↑(↑(Y.restrict (U := pullback f.base g.base) sorry) : TopCat) : Type u_1),
                  (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) :
              (a : (↑(↑(Y.restrict sorry) : TopCat) : Type u_1)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
            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) sorry) : TopCat))
                (PresheafedSpace.Hom.base (Y.ofRestrict sorry ≫ g.toHom)) :
              (a : (↑(↑(Y.restrict sorry) : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
            x))
        (eqToHom sorry)
        (g.stalkMap
            ((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) sorry) : TopCat))
                  (PresheafedSpace.Hom.base (Y.ofRestrict sorry)) :
                (a : (↑(↑(Y.restrict sorry) : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
              x) ≫
          PresheafedSpace.Hom.stalkMap (Y.ofRestrict sorry) x)))
Tactic: rw [this]