-- 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 : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
i : ℕ
a : ↥(𝒜 i)
b : A
hb : b ∈ 𝒜 i
hb' : b ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal
toIsLocalizationMap : (↑a : A) * b ^ (m - 1) ∈ 𝒜 (i * m)
⊢ ∃ (x_1 :
    (A⁰_ f) ×
      ↥(Ideal.primeCompl
          (PrimeSpectrum.asIdeal
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  carrier) (X :=
                  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                          ⋯).toPresheafedSpace :
                    TopCat))
                  (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
                (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                  (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
              x)))),
    HMul.hMul (α := AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) (β :=
        AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk
          { deg := i, num := a, den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) b hb, den_mem := hb' :
            NumDenSameDeg 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl })
        ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
              (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
            (↑x_1.2 : A⁰_ f) :
          AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) =
      (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        x_1.1
have toIsLocalizationMap₁ : HomogeneousLocalization.val
    (HMul.hMul (α := AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) (β :=
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
      (HomogeneousLocalization.mk
        { deg := i, num := a, den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) b hb, den_mem := hb' :
          NumDenSameDeg 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl })
      ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
            (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
          (↑(HomogeneousLocalization.mk
                    { deg := i * m, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (i * m)) ((↑a : A) * b ^ (m - 1)) sorry,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (i * m)) (f ^ i) sorry, den_mem := sorry :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) },
                  Subtype.mk (p := fun (x_1 : A⁰_ f) ↦
                    Membership.mem (γ := Submonoid (A⁰_ f))
                      (Ideal.primeCompl
                        (PrimeSpectrum.asIdeal
                          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
                                (CC := carrier) (X :=
                                (↑(Proj.restrict (U :=
                                        Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                                        sorry).toPresheafedSpace :
                                  TopCat))
                                (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
                              (a : (↑(↑(Proj.restrict sorry).toPresheafedSpace : TopCat) : Type u_1)) →
                                (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
                            x)))
                      x_1)
                    (HomogeneousLocalization.mk
                      { deg := i * m, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (i * m)) (b ^ m) sorry,
                        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (i * m)) (f ^ i) sorry, den_mem := sorry :
                        NumDenSameDeg 𝒜 (Submonoid.powers f) })
                    sorry).2 :
            A⁰_ f) :
        AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)) =
  HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
        (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
      (HomogeneousLocalization.mk
            { deg := i * m, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (i * m)) ((↑a : A) * b ^ (m - 1)) sorry,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (i * m)) (f ^ i) sorry, den_mem := sorry },
          Subtype.mk (p := fun (x_1 : A⁰_ f) ↦
            Membership.mem (γ := Submonoid (A⁰_ f))
              (Ideal.primeCompl
                (PrimeSpectrum.asIdeal
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                        carrier) (X :=
                        (↑(Proj.restrict (U :=
                                Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                                sorry).toPresheafedSpace :
                          TopCat))
                        (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
                      (a : (↑(↑(Proj.restrict sorry).toPresheafedSpace : TopCat) : Type u_1)) →
                        (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
                    x)))
              x_1)
            (HomogeneousLocalization.mk
              { deg := i * m, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (i * m)) (b ^ m) sorry,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (i * m)) (f ^ i) sorry, den_mem := sorry })
            sorry).1)
Tactic: refine ⟨⟨HomogeneousLocalization.mk ⟨i * m, ⟨a * b ^ (m - 1), ?_⟩,
        ⟨f ^ i, SetLike.pow_mem_graded _ f_deg⟩, ⟨_, rfl⟩⟩,
      ⟨HomogeneousLocalization.mk ⟨i * m, ⟨b ^ m, mul_comm m i ▸ SetLike.pow_mem_graded _ hb⟩,
        ⟨f ^ i, SetLike.pow_mem_graded _ f_deg⟩, ⟨_, rfl⟩⟩,
        (mk_mem_toSpec_base_apply _ _ _).not.mpr <| x.1.1.toIdeal.primeCompl.pow_mem hb' m⟩⟩,
        val_injective _ ?_⟩