-- 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 x_1 : A⁰_ f
h :
  ∀ (x_2 : ↥(unop (op (pbo f)))),
    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_3 : ↥(unop (op (pbo f)))) ↦
                  (HomogeneousLocalization.mapId 𝒜 ⋯ :
                      (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                        HomogeneousLocalization 𝒜
                          (↑x_3 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
                    (x * x_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_2) =
      HomogeneousLocalization.val
        ((↑(HMul.hMul (α :=
                (↑(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_3 : ↥(unop (op (pbo f)))) ↦
                    (HomogeneousLocalization.mapId 𝒜 ⋯ :
                        (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                          HomogeneousLocalization 𝒜
                            (↑x_3 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
                      x)
                  ⋯)
                (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)
                      x_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_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_2 : ↥(unop (op (pbo f)))) ↦
        (HomogeneousLocalization.mapId 𝒜 ⋯ :
            (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
              HomogeneousLocalization 𝒜
                (↑x_2 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
          (x * x_1))
      ⋯ =
    HMul.hMul (α :=
      (↑(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_2 : ↥(unop (op (pbo f)))) ↦
          (HomogeneousLocalization.mapId 𝒜 ⋯ :
              (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                HomogeneousLocalization 𝒜
                  (↑x_2 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
            x)
        ⋯)
      (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)
            x_1)
        ⋯)

Tactic:
ext