-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
e : X ≅ Y
y : (↑Y.toTopCat : Type u)
z :
  (↑(Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              e.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  e.inv.base :
                (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
              y :
            (↑(↑X.toPresheafedSpace : TopCat) : Type u)))) :
    Type u)
⊢ Eq (α := (↑(Y.presheaf.stalk y) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.stalkMap e.inv y) :
          (a :
              (↑(X.presheaf.stalk
                    ((ConcreteCategory.hom e.inv.base :
                        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
                      y)) :
                Type u)) →
            (↑(Y.presheaf.stalk y) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X :=
                Y.presheaf.stalk
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) e.hom.base :
                      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            carrier) e.inv.base :
                          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) →
                            (↑(↑X.toPresheafedSpace : TopCat) : Type u))
                        y :
                      (↑(↑X.toPresheafedSpace : TopCat) : Type u))))
                (Hom.stalkMap e.hom
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) e.inv.base :
                      (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
                    y)) :
              (a :
                  (↑(Y.presheaf.stalk
                        ((ConcreteCategory.hom e.hom.base :
                            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                              (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                          ((ConcreteCategory.hom e.inv.base :
                              (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) →
                                (↑(↑X.toPresheafedSpace : TopCat) : Type u))
                            y))) :
                    Type u)) →
                (↑(X.presheaf.stalk
                      ((ConcreteCategory.hom e.inv.base :
                          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) →
                            (↑(↑X.toPresheafedSpace : TopCat) : Type u))
                        y)) :
                  Type u))
            z :
          (↑(X.presheaf.stalk
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      e.inv.base :
                    (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
                  y)) :
            Type u)) :
      (↑(Y.presheaf.stalk y) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X :=
            Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    e.hom.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        e.inv.base :
                      (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
                    y :
                  (↑(↑X.toPresheafedSpace : TopCat) : Type u))))
            (Y.presheaf.stalkSpecializes ⋯) :
          (a :
              (↑(Y.presheaf.stalk
                    ((ConcreteCategory.hom e.hom.base :
                        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                      ((ConcreteCategory.hom e.inv.base :
                          (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) →
                            (↑(↑X.toPresheafedSpace : TopCat) : Type u))
                        y))) :
                Type u)) →
            (↑(Y.presheaf.stalk y) : Type u))
        z :
      (↑(Y.presheaf.stalk y) : Type u))

Tactic:
DFunLike.congr_fun (CommRingCat.hom_ext_iff.mp (stalkMap_hom_inv e y)) z

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