-- 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
⊢ 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)) ⋯,
                        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (i * m)) (f ^ i) ⋯, den_mem := ⋯ :
                        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))
                                          ⋯).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)))
                        x_1)
                      (HomogeneousLocalization.mk
                        { deg := i * m, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (i * m)) (b ^ m) ⋯,
                          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (i * m)) (f ^ i) ⋯, den_mem := ⋯ :
                          NumDenSameDeg 𝒜 (Submonoid.powers f) })
                      ⋯).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)) ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (i * m)) (f ^ i) ⋯, den_mem := ⋯ },
            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))
                                  ⋯).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)))
                x_1)
              (HomogeneousLocalization.mk
                { deg := i * m, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (i * m)) (b ^ m) ⋯,
                  den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (i * m)) (f ^ i) ⋯, den_mem := ⋯ })
              ⋯).1)
have toIsLocalizationMap : Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
  ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
        (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
      (f ^ i * ((↑a : A) * b ^ m)) :
    Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
  ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
        (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
      (b * f ^ i * ((↑a : A) * b ^ (m - 1))) :
    Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
Tactic: simp only [RingHom.algebraMap_toAlgebra, map_mk, GradedRingHom.id_apply, val_mul, val_mk,
        mk_eq_mk', ← IsLocalization.mk'_mul, Submonoid.mk_mul_mk, IsLocalization.mk'_eq_iff_eq]