-- 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
s : PullbackCone f g
x : (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u_1)
this :
  Eq (α :=
    Y.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))
              (PresheafedSpace.Hom.base
                (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                    (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯) ≫
                  (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).snd)) :
            (a : (↑(↑(PullbackCone.mk s.fst.toHom s.snd.toHom ⋯).pt : TopCat) : Type u_1)) →
              (↑(↑Y.toPresheafedSpace : 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 ⋯) ≫
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).snd)
      x)
    (CategoryStruct.comp (Y :=
      Y.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 :=
              (↑Y.toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base (PullbackCone.snd (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))) :
            (a : (↑(↑(PullbackCone.mk s.fst.toHom s.snd.toHom ⋯).pt : TopCat) : Type u_1)) →
              (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
          x))
      (eqToHom ⋯) (PresheafedSpace.Hom.stalkMap (PullbackCone.snd (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)) x))
⊢ Eq (α :=
    Y.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))
              (PresheafedSpace.Hom.base
                (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                    (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯) ≫
                  (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).snd)) :
            (a : (↑(↑(PullbackCone.mk s.fst.toHom s.snd.toHom ⋯).pt : TopCat) : Type u_1)) →
              (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
          x) ⟶
      s.pt.presheaf.stalk x)
    (PresheafedSpace.Hom.stalkMap
      (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯) ≫
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).snd)
      x)
    (eqToHom ⋯ ≫ s.snd.stalkMap x)

Tactic:
change _ = _ ≫ s.snd.1.stalkMap x at this

Premises used: AlgebraicGeometry.PresheafedSpace.Hom.stalkMap, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, CategoryTheory.Limits.PullbackCone.snd