-- 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
h :
  ∀ (x : ↥(unop (op (pbo f)))),
    Eq (α :=
      Localization (M := A) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
      (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
        ((↑(Subtype.mk (p :=
                fun
                  (f_1 :
                    (x : ↥(unop (op (pbo f)))) →
                      (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                          HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                        (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))) ↦
                PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T :=
                  fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                  HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                  (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                      HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal) (isLocallyFraction 𝒜) :
                    PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜)
                      fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                      HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                  f_1)
                (fun (x : ↥(unop (op (pbo f)))) ↦
                  (HomogeneousLocalization.mapId 𝒜 ⋯ :
                      (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                        HomogeneousLocalization 𝒜
                          (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
                    1)
                ⋯) :
            (x : ↥(unop (op (pbo f)))) →
              (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                  HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
          x))
      (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
        ((↑1 :
            (x : ↥(unop (op (pbo f)))) →
              (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                  HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
          x))
⊢ Eq.{u_1 + 1} (α :=
    (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
              (CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
              (structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
            (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
          (op (pbo f) : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
      Type u_1))
    (Subtype.mk (p :=
      fun
        (f_1 :
          (x : ↥(unop (op (pbo f)))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
              (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))) ↦
      PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
        HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
        (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
            HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal) (isLocallyFraction 𝒜) :
          PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
            HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
        f_1)
      (fun (x : ↥(unop (op (pbo f)))) ↦
        (HomogeneousLocalization.mapId 𝒜 ⋯ :
            (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
              HomogeneousLocalization 𝒜
                (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
          1)
      ⋯)
    1

Tactic:
ext