-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
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 : ↥(unop (op (pbo f)))
s : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
obtain :
  ∀ (n : ℕ) (hn : f ^ n = (↑s.den : A)),
    ∃ (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)
                  (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))))))
⊢ ∃ (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)
                (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 ⟨n, hn : f ^ n = s.den.1⟩ := s.den_mem

Premises used: HomogeneousLocalization.NumDenSameDeg.den_mem, HomogeneousLocalization.NumDenSameDeg.den, Subtype.val