-- 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 :
  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)
        ((↑z.den : A) * (↑y.num : A)) :
      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)
        ((↑y.den : A) * (↑z.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
c : A
hcx : c ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl
i : ℕ
hi :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) c : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) ∉
    (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal
hc :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                        x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                    A) *
                  ((↑z.den : A) * (↑y.num : A))) :
              ⨁ (i : ℕ), ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          (i + z.deg + y.deg)) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                        x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                    A) *
                  ((↑y.den : A) * (↑z.num : A))) :
              ⨁ (i : ℕ), ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          (i + y.deg + z.deg)) :
      A)
b_mem :
  ∀
    (hc :
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                        (↑(Subtype.mk (p := fun (x_1 : A) ↦
                              x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                          A) :
                      ⨁ (i : ℕ), ↥(𝒜 i)) :
                    (a : ℕ) → ↥(𝒜 a))
                  i) :
              A) *
            (↑z.den : A) *
          (↑y.num : A) =
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                      ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                              x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                          A) *
                        (↑y.den : A)) :
                    ⨁ (i : ℕ), ↥(𝒜 i)) :
                  (a : ℕ) → ↥(𝒜 a))
                (i + y.deg)) :
            A) *
          (↑z.num : A)),
    (↑y.den : A) ∈ 𝒜 y.deg
b_mem₁ :
  ∀
    (hc :
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                        (↑(Subtype.mk (p := fun (x_1 : A) ↦
                              x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                          A) :
                      ⨁ (i : ℕ), ↥(𝒜 i)) :
                    (a : ℕ) → ↥(𝒜 a))
                  i) :
              A) *
            (↑z.den : A) *
          (↑y.num : A) =
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                    ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                              x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                          A) *
                        (↑y.den : A) *
                      (↑z.num : A)) :
                  ⨁ (i : ℕ), ↥(𝒜 i)) :
                (a : ℕ) → ↥(𝒜 a))
              (i + y.deg + z.deg)) :
          A)),
    (↑z.num : A) ∈ 𝒜 z.deg
b_mem₂ :
  ∀
    (hc :
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                      ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                              x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                          A) *
                        (↑z.den : A)) :
                    ⨁ (i : ℕ), ↥(𝒜 i)) :
                  (a : ℕ) → ↥(𝒜 a))
                (i + z.deg)) :
            A) *
          (↑y.num : A) =
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                    ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                            x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                        A) *
                      ((↑y.den : A) * (↑z.num : A))) :
                  ⨁ (i : ℕ), ↥(𝒜 i)) :
                (a : ℕ) → ↥(𝒜 a))
              (i + y.deg + z.deg)) :
          A)),
    (↑z.den : A) ∈ 𝒜 z.deg
b_mem₃ :
  ∀
    (hc :
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                    ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                              x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                          A) *
                        (↑z.den : A) *
                      (↑y.num : A)) :
                  ⨁ (i : ℕ), ↥(𝒜 i)) :
                (a : ℕ) → ↥(𝒜 a))
              (i + z.deg + y.deg)) :
          A) =
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                    ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                            x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                        A) *
                      ((↑y.den : A) * (↑z.num : A))) :
                  ⨁ (i : ℕ), ↥(𝒜 i)) :
                (a : ℕ) → ↥(𝒜 a))
              (i + y.deg + z.deg)) :
          A)),
    (↑y.num : A) ∈ 𝒜 y.deg
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) c : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) *
      ((↑z.den : A) * (↑y.num : A)) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) c : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) *
      ((↑y.den : A) * (↑z.num : A))

Tactic:
rwa [← mul_assoc, coe_decompose_mul_add_of_right_mem, coe_decompose_mul_add_of_right_mem,
        ← mul_assoc, coe_decompose_mul_add_of_right_mem, coe_decompose_mul_add_of_right_mem,
        mul_assoc, mul_assoc] at hc

Premises used: mul_assoc, DirectSum.coe_decompose_mul_add_of_right_mem