-- 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
⊢ IsUnit
    (HMul.hMul (α := (↑(X.presheaf.stalk 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 :=
              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))
          t :
        (↑(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))
          t' :
        (↑(X.presheaf.stalk x) : Type u)))

Tactic:
exact ht.mul <| (IsLocalization.map_units (R := Γ.obj (op X)) S s).map _

Premises used: CommRingCat.carrier, IsUnit.mul, IsLocalization.map_units, IsUnit.map