-- 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
s : PullbackCone f g
x : (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u_1)
this :
  Eq (α :=
    (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).pt.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) (X :=
              (↑(Cone.pt (F := cospan f.toHom g.toHom) (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)) : TopCat)) (Y :=
              (↑(PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).pt : TopCat))
              (PresheafedSpace.Hom.base
                (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                  (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))) :
            (a : (↑(↑(PullbackCone.mk s.fst.toHom s.snd.toHom ⋯).pt : TopCat) : Type u_1)) →
              (↑(↑(PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).pt : TopCat) : Type u_1))
          x) ⟶
      TopCat.Presheaf.stalk
        (PresheafedSpace.presheaf (Cone.pt (F := cospan f.toHom g.toHom) (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)))
        x)
    (PresheafedSpace.Hom.stalkMap
      (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
        (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))
      x)
    (inv
        (PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).snd
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) (X :=
                (↑(Cone.pt (F := cospan f.toHom g.toHom) (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)) : TopCat)) (Y :=
                (↑(PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).pt : TopCat))
                (PresheafedSpace.Hom.base
                  (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                    (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))) :
              (a : (↑(↑(PullbackCone.mk s.fst.toHom s.snd.toHom ⋯).pt : TopCat) : Type u_1)) →
                (↑(↑(PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).pt : TopCat) : Type u_1))
            x)) ≫
      eqToHom ⋯ ≫ s.snd.stalkMap x)
⊢ IsLocalHom (R :=
    (↑((pullbackConeOfLeft f g).pt.presheaf.stalk
          (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) (X := (↑s.pt.toPresheafedSpace : TopCat)) (Y :=
                  (↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base
                      (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                        (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)) :
                    (↑s.pt.toPresheafedSpace : TopCat) ⟶ (↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat)) :
                C((↑(↑s.pt.toPresheafedSpace : TopCat) : Type u_1),
                  (↑(↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat) : Type u_1))) :
              (a : (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u_1)) →
                (↑(↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat) : Type u_1))
            x)) :
      Type u_1))
    (S := (↑(s.pt.presheaf.stalk x) : Type u_1)) (F :=
    (↑((pullbackConeOfLeft f g).pt.presheaf.stalk
            (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    TopCat.carrier) (X := (↑s.pt.toPresheafedSpace : TopCat)) (Y :=
                    (↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat))
                    (PresheafedSpace.Hom.base
                        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)) :
                      (↑s.pt.toPresheafedSpace : TopCat) ⟶ (↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat)) :
                  C((↑(↑s.pt.toPresheafedSpace : TopCat) : Type u_1),
                    (↑(↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat) : Type u_1))) :
                (a : (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u_1)) →
                  (↑(↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat) : Type u_1))
              x)) :
        Type u_1) →+*
      (↑(s.pt.presheaf.stalk x) : Type u_1))
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))
        x))
have refine_1 : IsLocalHom (R :=
  (↑((pullbackConeOfLeft f g).pt.presheaf.stalk
        (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) (X := (↑s.pt.toPresheafedSpace : TopCat)) (Y :=
                (↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base
                    (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                      (PullbackCone.mk s.fst.toHom s.snd.toHom sorry)) :
                  (↑s.pt.toPresheafedSpace : TopCat) ⟶ (↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat)) :
              C((↑(↑s.pt.toPresheafedSpace : TopCat) : Type u_1),
                (↑(↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat) : Type u_1))) :
            (a : (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat) : Type u_1))
          x)) :
    Type u_1))
  (S := (↑(s.pt.presheaf.stalk x) : Type u_1)) (F :=
  (↑((pullbackConeOfLeft f g).pt.presheaf.stalk
          (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) (X := (↑s.pt.toPresheafedSpace : TopCat)) (Y :=
                  (↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base
                      (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                        (PullbackCone.mk s.fst.toHom s.snd.toHom sorry)) :
                    (↑s.pt.toPresheafedSpace : TopCat) ⟶ (↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat)) :
                C((↑(↑s.pt.toPresheafedSpace : TopCat) : Type u_1),
                  (↑(↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat) : Type u_1))) :
              (a : (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u_1)) →
                (↑(↑(pullbackConeOfLeft f g).pt.toPresheafedSpace : TopCat) : Type u_1))
            x)) :
      Type u_1) →+*
    (↑(s.pt.presheaf.stalk x) : Type u_1))
  (CommRingCat.Hom.hom
    (inv
        (PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).snd
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) (X :=
                (↑(Cone.pt (F := cospan f.toHom g.toHom) (PullbackCone.mk s.fst.toHom s.snd.toHom sorry)) : TopCat)) (Y :=
                (↑(PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).pt : TopCat))
                (PresheafedSpace.Hom.base
                  (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                    (PullbackCone.mk s.fst.toHom s.snd.toHom sorry))) :
              (a : (↑(↑(PullbackCone.mk s.fst.toHom s.snd.toHom sorry).pt : TopCat) : Type u_1)) →
                (↑(↑(PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).pt : TopCat) : Type u_1))
            x)) ≫
      eqToHom sorry ≫ s.snd.stalkMap x))
Tactic: rw [this]