-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
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))
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))
                                  ⋯).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 := m * i, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (c ^ m) ⋯,
                  den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                  NumDenSameDeg 𝒜 (Submonoid.powers f) })
              ⋯) :
          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))
                                  ⋯).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 := m * i, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (c ^ m) ⋯,
                  den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                  NumDenSameDeg 𝒜 (Submonoid.powers f) })
              ⋯) :
          A⁰_ f) *
        HomogeneousLocalization.mk z)
⊢ ∃ (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

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 _ ?_⟩