-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : A⁰_ f
e :
  Eq (α := AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        y :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        z :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
⊢ ∃ (c :
    ↥(Ideal.primeCompl
        (PrimeSpectrum.asIdeal
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (X :=
                (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                        ⋯).toPresheafedSpace :
                  TopCat))
                (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
              (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
            x)))),
    (↑c : A⁰_ f) * y = (↑c : A⁰_ f) * z
have toIsLocalizationMap : ∀ (y : NumDenSameDeg 𝒜 (Submonoid.powers f))
  (e :
    Eq (α := AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
      ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
            (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
          (HomogeneousLocalization.mk y) :
        AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
      ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
            (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
          z :
        AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)),
  ∃ (c :
    ↥(Ideal.primeCompl
        (PrimeSpectrum.asIdeal
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (X :=
                (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                        sorry).toPresheafedSpace :
                  TopCat))
                (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
              (a : (↑(↑(Proj.restrict sorry).toPresheafedSpace : TopCat) : Type u_1)) →
                (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
            x)))),
    (↑c : A⁰_ f) * HomogeneousLocalization.mk y = (↑c : A⁰_ f) * z
Tactic: obtain ⟨y, rfl⟩ := HomogeneousLocalization.mk_surjective y
Cleared hypotheses: y, e