-- 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 :
  Eq (α := Localization (Submonoid.powers f))
    ((algebraMap A (Localization (Submonoid.powers f)) : (a : A) → Localization (Submonoid.powers f))
        (f ^ i * ((↑z.den : A) * (c ^ m * (↑y.num : A)))) :
      Localization (Submonoid.powers f))
    ((algebraMap A (Localization (Submonoid.powers f)) : (a : A) → Localization (Submonoid.powers f))
        (f ^ i * ((↑y.den : A) * (c ^ m * (↑z.num : A)))) :
      Localization (Submonoid.powers f))
⊢ 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)

Tactic:
simp only [val_mul, val_mk, mk_eq_mk', ← IsLocalization.mk'_mul, Submonoid.mk_mul_mk,
      IsLocalization.mk'_eq_iff_eq, mul_assoc]

Premises used: Localization.mk_eq_mk', mul_assoc, HomogeneousLocalization.val_mk, HomogeneousLocalization.val_mul, IsLocalization.mk'_eq_iff_eq, Submonoid.mk_mul_mk, IsLocalization.mk'_mul