-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
e : X ≅ Y
x : (↑X.toTopCat : Type u)
y :
  (↑(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))
          ((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))
              x :
            (↑(↑Y.toPresheafedSpace : TopCat) : Type u)))) :
    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 e.hom x) :
          (a :
              (↑(Y.presheaf.stalk
                    ((ConcreteCategory.hom e.hom.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
                  ((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))
                    ((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))
                        x :
                      (↑(↑Y.toPresheafedSpace : TopCat) : Type u))))
                (Hom.stalkMap e.inv
                  ((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))
                    x)) :
              (a :
                  (↑(X.presheaf.stalk
                        ((ConcreteCategory.hom e.inv.base :
                            (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) →
                              (↑(↑X.toPresheafedSpace : TopCat) : Type u))
                          ((ConcreteCategory.hom e.hom.base :
                              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                                (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                            x))) :
                    Type u)) →
                (↑(Y.presheaf.stalk
                      ((ConcreteCategory.hom e.hom.base :
                          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                            (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                        x)) :
                  Type u))
            y :
          (↑(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))
                  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
              ((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))
                ((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))
                    x :
                  (↑(↑Y.toPresheafedSpace : TopCat) : Type u))))
            (X.presheaf.stalkSpecializes ⋯) :
          (a :
              (↑(X.presheaf.stalk
                    ((ConcreteCategory.hom e.inv.base :
                        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
                      ((ConcreteCategory.hom e.hom.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))

Tactic:
DFunLike.congr_fun (CommRingCat.hom_ext_iff.mp (stalkMap_inv_hom e x)) y

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