-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens (↑Y.toTopCat : Type u)
x : ↥((Opens.map f.base).obj V)
a : (↑(Y.presheaf.obj (op V)) : Type u)
⊢ Eq (α := (↑(X.residueField (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X :=
            Y.residueField
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))))
            (residueFieldMap f (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) :
          (a :
              (↑(Y.residueField
                    ((ConcreteCategory.hom f.base :
                        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                      (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)))) :
                Type u)) →
            (↑(X.residueField (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Y.presheaf.obj (op V)) (Y :=
              Y.residueField
                (↑(Subtype.mk (p := fun (x : (↑Y.toTopCat : Type u)) ↦ x ∈ V)
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            TopCat.carrier) f.base :
                          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                            (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                        (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
                      ⋯) :
                  (↑Y.toTopCat : Type u)))
              (Y.evaluation
                (Subtype.mk (p := fun (x : (↑Y.toTopCat : Type u)) ↦ x ∈ V)
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        TopCat.carrier) f.base :
                      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                    (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
                  ⋯)) :
            (a : (↑(Y.presheaf.obj (op V)) : Type u)) →
              (↑(Y.residueField
                    (↑⟨(ConcreteCategory.hom f.base :
                              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                                (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                            (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)),
                          ⋯⟩ :
                      (↑Y.toTopCat : Type u))) :
                Type u))
          a) :
      (↑(X.residueField (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.evaluation x) :
          (a : (↑(X.presheaf.obj (op ((Opens.map f.base).obj V))) : Type u)) →
            (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Y.presheaf.obj (op V)) (f.c.app (op V)) :
            (a : (↑(Y.presheaf.obj (op V)) : Type u)) →
              (↑(((TopCat.Presheaf.pushforward CommRingCat f.base).obj X.presheaf).obj (op V)) : Type u))
          a) :
      (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))

Tactic:
simpa using congrFun (congrArg (DFunLike.coe ∘ CommRingCat.Hom.hom) <|
    evaluation_naturality f x) a

Premises used: CommRingCat.Hom.hom, congrArg, Function.comp, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, congrFun, DFunLike.coe