-- 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)
hf :
  Eq (α := (↑(X.residueField (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) : Type u))
    ((IsLocalRing.residue (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) : Type u) :
          (a : (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) : Type u)) →
            IsLocalRing.ResidueField (↑(X.presheaf.stalk (↑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 := X.presheaf.obj (op ((Opens.map f.base).obj V))) (Y :=
              X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
              (X.presheaf.germ ((Opens.map f.base).obj V) (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) ⋯) :
            (a : (↑(X.presheaf.obj (op ((Opens.map f.base).obj V))) : Type u)) →
              (↑(X.presheaf.stalk (↑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 :
            (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat f.base) X.presheaf).obj (op V)) : Type u))) :
      IsLocalRing.ResidueField (↑(X.presheaf.stalk (↑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)) ⋯)
                  (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))
⊢ Eq (α := (↑(X.residueField (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) : Type u))
    ((IsLocalRing.residue (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) : Type u) :
          (a : (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) : Type u)) →
            IsLocalRing.ResidueField (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u))) : Type u))
        ((CommRingCat.Hom.hom (Hom.stalkMap f (↑x : (↑(↑X.toPresheafedSpace : TopCat) : 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)) →
              (↑(X.presheaf.stalk (↑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)))
                        ⋯ :
                      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 :
            (↑(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))) :
      IsLocalRing.ResidueField (↑(X.presheaf.stalk (↑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)) ⋯)
                  (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:
rw [LocallyRingedSpace.stalkMap_germ_apply]

Premises used: AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply