-- 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 x_1 : A⁰_ f
⊢ 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))
      ⋯ =
    HAdd.hAdd (α :=
      (↑(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)
        ⋯)
have 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 𝒜 sorry :
                    (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                      HomogeneousLocalization 𝒜
                        (↑x_3 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
                  (x + x_1))
              sorry) :
          (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
      ((↑(HAdd.hAdd (α :=
              (↑(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 𝒜 sorry :
                      (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                        HomogeneousLocalization 𝒜
                          (↑x_3 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
                    x)
                sorry)
              (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 𝒜 sorry :
                      (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                        HomogeneousLocalization 𝒜
                          (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
                    x_1)
                sorry)) :
          (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)
Tactic: ext