-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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
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))
⊢ 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))

Tactic:
rw [← toStalk_stalkMap_toΓSpec, CommRingCat.comp_apply]

Premises used: CommRingCat.comp_apply, AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec