-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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 :
  Eq (α := (↑((Spec R).presheaf.stalk p) : Type u))
    ((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) :
          (a : (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u)) →
            (↑((Spec R).presheaf.stalk p) : 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)
          x s) :
      (↑((Spec R).presheaf.stalk p) : Type u))
    (0 : (↑((Spec R).presheaf.stalk p) : Type u))
refine_2 :
  ∀
    (hx :
      Eq (α := (↑((Spec R).presheaf.stalk p) : Type u))
        ((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) :
              (a : (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u)) →
                (↑((Spec R).presheaf.stalk p) : 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)) :
          (↑((Spec R).presheaf.stalk p) : Type u))
        (0 : (↑((Spec R).presheaf.stalk p) : Type u))),
    Eq (α := (↑((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)
        x s)
      0
⊢ Eq (α := (↑((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)
      x s)
    0
have refine_2₁ : ∀
  (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: rw [← RingHom.mem_ker, IsLocalization.mk'_eq_mul_mk'_one, Ideal.mul_unit_mem_iff_mem,
    RingHom.mem_ker] at hx
Cleared hypotheses: hx