-- 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
⊢ 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
have 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 𝒜 sorry :
                    (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                      HomogeneousLocalization 𝒜
                        (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
                  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))
    (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))
Tactic: ext