-- 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
s : A⁰_ f
x : ↥(unop (op (pbo f)))
⊢ ∃ (V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (_ : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V) (i :
    V ⟶ unop (op (pbo f))),
    PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
      HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
      (isFractionPrelocal 𝒜 :
        PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
          HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
      (U := V) fun (x : ↥V) ↦
      ((fun (x : ↥(unop (op (pbo f)))) ↦
            ((HomogeneousLocalization.mapId 𝒜 ⋯ :
                  (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                    HomogeneousLocalization 𝒜
                      (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
                s :
              HomogeneousLocalization 𝒜
                (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl))
          ((i : (a : ↥V) → ↥(unop (op (pbo f)))) x) :
        HomogeneousLocalization 𝒜
          (Ideal.primeCompl
            (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (σ := σ) (𝒜 := 𝒜)
              (ProjectiveSpectrum.asHomogeneousIdeal
                (↑((i : (a : ↥V) → ↥(unop (op (pbo f)))) x) : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))))))
have obtain : ∀ (s : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)),
  ∃ (V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (_ : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V) (i :
    V ⟶ unop (op (pbo f))),
    PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
      HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
      (isFractionPrelocal 𝒜 :
        PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
          HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
      (U := V) fun (x : ↥V) ↦
      ((fun (x : ↥(unop (op (pbo f)))) ↦
            ((HomogeneousLocalization.mapId 𝒜 sorry :
                  (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                    HomogeneousLocalization 𝒜
                      (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
                (HomogeneousLocalization.mk s) :
              HomogeneousLocalization 𝒜
                (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl))
          ((i : (a : ↥V) → ↥(unop (op (pbo f)))) x) :
        HomogeneousLocalization 𝒜
          (Ideal.primeCompl
            (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (σ := σ) (𝒜 := 𝒜)
              (ProjectiveSpectrum.asHomogeneousIdeal
                (↑((i : (a : ↥V) → ↥(unop (op (pbo f)))) x) : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))))))
Tactic: obtain ⟨s, rfl⟩ := HomogeneousLocalization.mk_surjective s
Cleared hypotheses: s