-- 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)
hf :
  ∀ (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))
⊢ Eq (α := Y.presheaf.obj (op V) ⟶ X.residueField (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
    (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))) :
      Y.presheaf.obj (op V) ⟶ X.residueField (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
    (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) ⟶ X.residueField (↑x : (↑X.toTopCat : Type u)))

Tactic:
ext a