-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
R : CommRingCat
H_1 :
  ∀ (I : Ideal (↑R : Type u)),
    I.IsPrime → ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
p : ↥(Spec R)
f : (↑R : Type u)
hf : f ∉ p.asIdeal
H : ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ p.asIdeal → ∃ (n : ℕ), f ^ n * x = 0
x : (↑R : Type u)
s : ↥(Submonoid.powers f)
hx :
  Membership.mem (γ := Ideal (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u))
    (RingHom.ker (F :=
      (fun (R S : CommRingCat.{u}) ↦ RingHom.{u, u} (↑R : Type u) (↑S : Type u))
        ((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) ((Spec R).presheaf.stalk p))
      (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) (X := (Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) (Y :=
        (Spec R).presheaf.stalk p) ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf)))
    (HMul.hMul (α :=
      (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (Spec.structureSheaf (↑R : Type u)))
            (Opposite.op (PrimeSpectrum.basicOpen f))) :
        Type u))
      (β :=
      (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (Spec.structureSheaf (↑R : Type u)))
            (Opposite.op (PrimeSpectrum.basicOpen f))) :
        Type u))
      ((algebraMap (↑R : Type u)
              (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
                    (ObjectProperty.FullSubcategory.obj (P :=
                      Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                      (Spec.structureSheaf (↑R : Type u)))
                    (Opposite.op (PrimeSpectrum.basicOpen f))) :
                Type u) :
            (a : (↑R : Type u)) →
              (↑((Spec.structureSheaf (↑R : Type u)).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u))
          x :
        (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (Spec.structureSheaf (↑R : Type u)))
              (Opposite.op (PrimeSpectrum.basicOpen f))) :
          Type u))
      (IsLocalization.mk'
          (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                  (Spec.structureSheaf (↑R : Type u)))
                (Opposite.op (PrimeSpectrum.basicOpen f))) :
            Type u)
          1 s :
        (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (Spec.structureSheaf (↑R : Type u)))
              (Opposite.op (PrimeSpectrum.basicOpen f))) :
          Type u)))
⊢ IsUnit (M := (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u))
    (IsLocalization.mk'
      (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (Spec.structureSheaf (↑R : Type u)))
            (Opposite.op (PrimeSpectrum.basicOpen f))) :
        Type u)
      1 s)

Tactic:
exact @isUnit_of_invertible _ _ _ (@IsLocalization.invertible_mk'_one ..)

Premises used: isUnit_of_invertible