-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑R : Type u)
inst : Algebra (↑R : Type u) (↑S : Type u)
h₁ :
  ∀ x ∈ p.asIdeal.primeCompl,
    IsUnit (M :=
      (↑(TopCat.Presheaf.stalk
            (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
              (TopCat.Presheaf.pushforward CommRingCat
                (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                (structureSheaf (↑S : Type u))))
            p) :
        Type u))
      ((algebraMap (↑R : Type u)
              (↑(TopCat.Presheaf.stalk
                    (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                      (TopCat.Presheaf.pushforward CommRingCat
                        (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                      (ObjectProperty.FullSubcategory.obj (P :=
                        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                        (structureSheaf (↑S : Type u))))
                    p) :
                Type u) :
            (a : (↑R : Type u)) →
              (↑(((TopCat.Presheaf.pushforward CommRingCat
                            (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                        (structureSheaf (↑S : Type u)).obj).stalk
                    p) :
                Type u))
          x :
        (↑(TopCat.Presheaf.stalk
              (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                (TopCat.Presheaf.pushforward CommRingCat
                  (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                  (structureSheaf (↑S : Type u))))
              p) :
          Type u))
h₂ :
  ∀
    (y :
      (↑(TopCat.Presheaf.stalk
            (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
              (TopCat.Presheaf.pushforward CommRingCat
                (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                (structureSheaf (↑S : Type u))))
            p) :
        Type u)),
    ∃ (x : (↑S : Type u) × ↥p.asIdeal.primeCompl),
      x.2 • y =
        (toPushforwardStalkAlgHom R S p :
            (a : (↑S : Type u)) →
              (↑(((TopCat.Presheaf.pushforward CommRingCat
                            (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                        (structureSheaf (↑S : Type u)).obj).stalk
                    p) :
                Type u))
          x.1
h₃ :
  ∀ (x : (↑S : Type u)),
    Eq (α :=
        (↑(TopCat.Presheaf.stalk
              (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                (TopCat.Presheaf.pushforward CommRingCat
                  (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                  (structureSheaf (↑S : Type u))))
              p) :
          Type u))
        ((toPushforwardStalkAlgHom R S p :
              (a : (↑S : Type u)) →
                (↑(((TopCat.Presheaf.pushforward CommRingCat
                              (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                          (structureSheaf (↑S : Type u)).obj).stalk
                      p) :
                  Type u))
            x :
          (↑(TopCat.Presheaf.stalk
                (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                  (TopCat.Presheaf.pushforward CommRingCat
                    (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                  (ObjectProperty.FullSubcategory.obj (P :=
                    Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                    (structureSheaf (↑S : Type u))))
                p) :
            Type u))
        (0 :
          (↑(TopCat.Presheaf.stalk
                (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                  (TopCat.Presheaf.pushforward CommRingCat
                    (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                  (ObjectProperty.FullSubcategory.obj (P :=
                    Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                    (structureSheaf (↑S : Type u))))
                p) :
            Type u)) →
      ∃ (m : ↥p.asIdeal.primeCompl), m • x = 0
⊢ IsLocalizedModule (M' :=
    (↑(TopCat.Presheaf.stalk
          (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
            (TopCat.Presheaf.pushforward CommRingCat
              (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
              (structureSheaf (↑S : Type u))))
          p) :
      Type u))
    p.asIdeal.primeCompl (AlgHom.toLinearMap (toPushforwardStalkAlgHom R S p))

Tactic:
apply IsLocalizedModule.mkOfAlgebra

Premises used: IsLocalizedModule.mkOfAlgebra