-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField (goal)
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))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              Y.presheaf.stalk
                ((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.presheaf.germ 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.presheaf.obj (op V) ⟶
                  Y.presheaf.stalk
                    ((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))))
              (CategoryStruct.comp (Y :=
                  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))))
                  (CommRingCat.ofHom
                    (IsLocalRing.residue
                      (↑(Y.presheaf.stalk
                            ((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)))) :
                        Type u)))
                  (CommRingCat.ofHom
                    (IsLocalRing.ResidueField.map
                      (CommRingCat.Hom.hom (Hom.stalkMap f (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)))))) :
                Y.presheaf.stalk
                    ((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))) ⟶
                  X.residueField (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)))) :
          (a : (↑(Y.presheaf.obj (op V)) : Type u)) →
            (↑(X.residueField (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) : Type u))
        a :
      (↑(X.residueField (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) : Type u))
    (((CommRingCat.Hom.hom
              (f.c.app (op V) ≫
                CategoryStruct.comp (Y := X.presheaf.stalk (↑x : (↑X.toTopCat : Type u)))
                  (X.presheaf.germ ((Opens.map f.base).obj V) (↑x : (↑X.toTopCat : Type u)) ⋯)
                  (CommRingCat.ofHom
                    (IsLocalRing.residue (↑(X.presheaf.stalk (↑x : (↑X.toTopCat : Type u))) : Type u)))) :
            (↑(Y.presheaf.obj (op V)) : Type u) →+*
              (↑(X.residueField (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) : Type u)) :
          (a : (↑(Y.presheaf.obj (op V)) : Type u)) →
            (↑(X.residueField (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) : Type u))
        a :
      (↑(X.residueField (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) : Type u))
have hf : 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))))
          (Y := X.residueField (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
          (CommRingCat.ofHom
            (IsLocalRing.ResidueField.map
              (CommRingCat.Hom.hom (Hom.stalkMap 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.stalk
              ((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 :=
            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))))
            (CommRingCat.ofHom
              (IsLocalRing.residue
                (↑(Y.presheaf.stalk
                      ((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)))) :
                  Type u))) :
          (a :
              (↑(Y.presheaf.stalk
                    ((ConcreteCategory.hom f.base :
                        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                      (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)))) :
                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)))) :
              Type u))
        (((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y :=
                Y.presheaf.stalk
                  ((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.presheaf.germ 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)))
                    sorry :
                  Y.presheaf.obj (op V) ⟶
                    Y.presheaf.stalk
                      ((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.presheaf.obj (op V)) : Type u) →+*
                (↑(Y.presheaf.stalk
                      ((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)))) :
                  Type u)) :
            (a : (↑(Y.presheaf.obj (op V)) : Type u)) →
              (↑(Y.presheaf.stalk
                    ((ConcreteCategory.hom f.base :
                        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                      (↑x : (↑(↑X.toPresheafedSpace : TopCat) : 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) (Y := X.residueField (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
            (CategoryStruct.comp (Y := X.presheaf.stalk (↑x : (↑X.toTopCat : Type u)))
                (X.presheaf.germ ((Opens.map f.base).obj V) (↑x : (↑X.toTopCat : Type u)) sorry)
                (CommRingCat.ofHom (IsLocalRing.residue (↑(X.presheaf.stalk (↑x : (↑X.toTopCat : Type u))) : Type u))) :
              X.presheaf.obj (op ((Opens.map f.base).obj V)) ⟶ X.residueField (↑x : (↑X.toTopCat : Type u))) :
          (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat f.base) X.presheaf).obj (op V)) : Type u) →+*
            (↑(X.residueField (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) : Type u)) :
        (a : (↑(((TopCat.Presheaf.pushforward CommRingCat f.base).obj X.presheaf).obj (op V)) : 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)) (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.toPresheafedSpace : TopCat) : Type u))) : Type u))
Tactic: simp only [CommRingCat.comp_apply]