-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (hypothesis)
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 + z.deg + y.deg)) :
      A)
⊢ (↑((((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))
have 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)
Tactic: conv_rhs at hc => rw [add_right_comm]
Cleared hypotheses: hc