-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
r_1 : (↑(Γ.obj (op X)) : Type u)
x : (↑X.toTopCat : Type u)
p : PrimeSpectrum (↑(Γ.obj (op X)) : Type u) := X.toΓSpecFun x
S : CommRingCat := stalk (TopCat.Sheaf.presheaf (structureSheaf (↑(Γ.obj (op X)) : Type u))) p
t : (↑S : Type u)
ht :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u))
    ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x) :
          (a :
              (↑((Spec.locallyRingedSpaceObj (Γ.obj (op X))).presheaf.stalk
                    ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base :
                        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                          (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
                      x)) :
                Type u)) →
            (↑(X.presheaf.stalk x) : Type u))
        t :
      (↑(X.presheaf.stalk x) : Type u))
r : (↑(Γ.obj (op X)) : Type u)
s : ↥p.asIdeal.primeCompl
t' : (↑S : Type u) :=
  (algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u) (↑S : Type u) :
      (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑S : Type u))
    (↑s : (↑(X.presheaf.obj (op ⊤)) : Type u))
he :
  t * t' =
    (algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u) (↑S : Type u) :
        (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑S : Type u))
      r
⊢ IsUnit (M := (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.Γgerm x) :
          (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        r :
      (↑(X.presheaf.stalk x) : Type u))
have map_nonunit : IsUnit (M := (↑(X.presheaf.stalk x) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X :=
          stalk (X := PrimeSpectrum.Top (↑(unop (op (Γ.obj (op X)))) : Type u))
            (structurePresheafInCommRingCat (↑(unop (op (Γ.obj (op X)))) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) X.toΓSpecSheafedSpace.hom.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                  (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
              x))
          (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x) :
        (a :
            (↑((structurePresheafInCommRingCat (↑(unop (op (Γ.obj (op X)))) : Type u)).stalk
                  ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base :
                      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                        (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).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.obj (op ⊤)) (Y :=
              stalk (X := PrimeSpectrum.Top (↑(unop (op (Γ.obj (op X)))) : Type u))
                (structurePresheafInCommRingCat (↑(unop (op (Γ.obj (op X)))) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                      TopCat.carrier) X.toΓSpecSheafedSpace.hom.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                      (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
                  x))
              (toStalk (↑(unop (op (Γ.obj (op X)))) : Type u)
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                      TopCat.carrier) X.toΓSpecSheafedSpace.hom.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                      (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
                  x)) :
            (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) →
              (↑((structurePresheafInCommRingCat (↑(unop (op (Γ.obj (op X)))) : Type u)).stalk
                    ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base :
                        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                          (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
                      x)) :
                Type u))
          r :
        (↑(stalk (X := PrimeSpectrum.Top (↑(unop (op (Γ.obj (op X)))) : Type u))
              (structurePresheafInCommRingCat (↑(unop (op (Γ.obj (op X)))) : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) X.toΓSpecSheafedSpace.hom.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                    (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
                x)) :
          Type u)) :
    (↑(X.presheaf.stalk x) : Type u))
Tactic: rw [← toStalk_stalkMap_toΓSpec, CommRingCat.comp_apply]