-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
x x' : (↑X.toTopCat : Type u)
h : x ⤳ x'
y :
  (↑(Y.presheaf.stalk
        ((Hom.hom f.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x')) :
    Type u)
⊢ Eq (α := (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.stalkMap f x) :
          (a :
              (↑(Y.presheaf.stalk
                    ((ConcreteCategory.hom f.base :
                        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                      x)) :
                Type u)) →
            (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X :=
                Y.presheaf.stalk
                  ((Hom.hom f.base :
                      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                    x'))
                (Y.presheaf.stalkSpecializes ⋯) :
              (a :
                  (↑(Y.presheaf.stalk
                        ((Hom.hom f.base :
                            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                              (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                          x')) :
                    Type u)) →
                (↑(Y.presheaf.stalk
                      ((Hom.hom f.base :
                          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                            (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                        x)) :
                  Type u))
            y :
          (↑(Y.presheaf.stalk
                ((Hom.hom f.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                  x)) :
            Type u)) :
      (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.stalk x') (X.presheaf.stalkSpecializes h) :
          (a : (↑(X.presheaf.stalk x') : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.stalkMap f x') :
              (a :
                  (↑(Y.presheaf.stalk
                        ((ConcreteCategory.hom f.base :
                            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                              (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                          x')) :
                    Type u)) →
                (↑(X.presheaf.stalk x') : Type u))
            y :
          (↑(X.presheaf.stalk x') : Type u)) :
      (↑(X.presheaf.stalk x) : Type u))

Tactic:
DFunLike.congr_fun (CommRingCat.hom_ext_iff.mp (stalkSpecializes_stalkMap f x x' h)) y

Premises used: DFunLike.congr_fun, CommRingCat.hom_ext_iff, Iff.mp, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap