-- 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 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e_1 :
  Eq (α := AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk y) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk z) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal
e : c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
⊢ ∃ (c :
    ↥(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)))),
    (↑c : A⁰_ f) * HomogeneousLocalization.mk y = (↑c : A⁰_ f) * HomogeneousLocalization.mk z
have toIsLocalizationMap : HomogeneousLocalization.val
    ((↑(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 := m * i, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (c ^ m) sorry,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
                NumDenSameDeg 𝒜 (Submonoid.powers f) })
            sorry) :
        A⁰_ f) *
      HomogeneousLocalization.mk y) =
  HomogeneousLocalization.val
    ((↑(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 := m * i, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (c ^ m) sorry,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
                NumDenSameDeg 𝒜 (Submonoid.powers f) })
            sorry) :
        A⁰_ f) *
      HomogeneousLocalization.mk z)
Tactic: refine ⟨⟨HomogeneousLocalization.mk ⟨m * i, ⟨c ^ m, SetLike.pow_mem_graded _ hc⟩,
      ⟨f ^ i, mul_comm m i ▸ SetLike.pow_mem_graded _ f_deg⟩, ⟨_, rfl⟩⟩,
      (mk_mem_toSpec_base_apply _ _ _).not.mpr <| x.1.1.toIdeal.primeCompl.pow_mem hc' _⟩,
      val_injective _ ?_⟩