-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑R : Type u)
inst : Algebra (↑R : Type u) (↑S : Type u)
x : (↑R : Type u)
hx : x ∈ p.asIdeal.primeCompl
⊢ IsUnit (M :=
    (↑(Functor.obj (C :=
          TopCat.Presheaf CommRingCat
            (↑(Spec.sheafedSpaceObj (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
          (TopCat.Presheaf.stalkFunctor CommRingCat p)
          (Functor.obj
            (TopCat.Presheaf.pushforward CommRingCat
              (PresheafedSpace.Hom.base
                (InducedCategory.Hom.hom
                  (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))))
            (Spec.sheafedSpaceObj (CommRingCat.of (↑S : Type u))).presheaf)) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X :=
            Functor.obj (TopCat.Presheaf.stalkFunctor CommRingCat p)
              (Spec.sheafedSpaceObj (CommRingCat.of (↑R : Type u))).presheaf)
            (Y :=
            Functor.obj (C :=
              TopCat.Presheaf CommRingCat
                (↑(Spec.sheafedSpaceObj (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
              (TopCat.Presheaf.stalkFunctor CommRingCat p)
              (Functor.obj
                (TopCat.Presheaf.pushforward CommRingCat
                  (PresheafedSpace.Hom.base
                    (InducedCategory.Hom.hom
                      (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))))
                (Spec.sheafedSpaceObj (CommRingCat.of (↑S : Type u))).presheaf))
            (CategoryTheory.Functor.map (TopCat.Presheaf.stalkFunctor CommRingCat p)
              (PresheafedSpace.Hom.c
                (InducedCategory.Hom.hom
                  (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))))) :
          (a :
              (↑((TopCat.Presheaf.stalkFunctor CommRingCat p).obj
                    (Spec.sheafedSpaceObj (CommRingCat.of (↑R : Type u))).presheaf) :
                Type u)) →
            (↑((TopCat.Presheaf.stalkFunctor CommRingCat p).obj
                  ((TopCat.Presheaf.pushforward CommRingCat
                        (Spec.sheafedSpaceMap
                              (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))).hom.base).obj
                    (Spec.sheafedSpaceObj (CommRingCat.of (↑S : Type u))).presheaf)) :
              Type u))
        (((toStalk (↑R : Type u) p).hom' :
              (a : (↑(CommRingCat.of (↑R : Type u)) : Type u)) →
                (↑((structurePresheafInCommRingCat (↑R : Type u)).stalk p) : Type u))
            x :
          (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u)) p) : Type u)) :
      (↑(Functor.obj (C :=
            TopCat.Presheaf CommRingCat
              (↑(Spec.sheafedSpaceObj (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
            (TopCat.Presheaf.stalkFunctor CommRingCat p)
            (Functor.obj
              (TopCat.Presheaf.pushforward CommRingCat
                (PresheafedSpace.Hom.base
                  (InducedCategory.Hom.hom
                    (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))))
              (Spec.sheafedSpaceObj (CommRingCat.of (↑S : Type u))).presheaf)) :
        Type u))

Tactic:
exact (IsLocalization.map_units ((structureSheaf R).presheaf.stalk p) ⟨x, hx⟩).map _

Premises used: CommRingCat.carrier, TopCat.Presheaf.stalk, Subtype.mk, IsLocalization.map_units, AlgebraicGeometry.Spec.structureSheaf, IsUnit.map, TopCat.Sheaf.presheaf