-- Module: Mathlib.RingTheory.GradedAlgebra.Basic
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst : Semiring A
inst_1 : DecidableEq ι
inst_2 : AddCommMonoid ι
inst_3 : PartialOrder ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : SetLike σ A
inst_6 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_7 : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
m : A
refine_2 :
  ∀ (m' : A),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * m) :
                  ⨁ (i : ι), ↥(𝒜 i)) :
                (a : ι) → ↥(𝒜 a))
              0) :
          A) =
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) :
                    ⨁ (i : ι), ↥(𝒜 i)) :
                  (a : ι) → ↥(𝒜 a))
                0) :
            A) *
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) m : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) →
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * m') :
                    ⨁ (i : ι), ↥(𝒜 i)) :
                  (a : ι) → ↥(𝒜 a))
                0) :
            A) =
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) :
                      ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ι) → ↥(𝒜 a))
                  0) :
              A) *
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) m' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) →
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                      ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * (m + m')) :
                    ⨁ (i : ι), ↥(𝒜 i)) :
                  (a : ι) → ↥(𝒜 a))
                0) :
            A) =
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) :
                      ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ι) → ↥(𝒜 a))
                  0) :
              A) *
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (m + m') : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
⊢ ∀ (m' : A),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * m) :
                  ⨁ (i : ι), ↥(𝒜 i)) :
                (a : ι) → ↥(𝒜 a))
              0) :
          A) =
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) :
                    ⨁ (i : ι), ↥(𝒜 i)) :
                  (a : ι) → ↥(𝒜 a))
                0) :
            A) *
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) m : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) →
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * m') :
                    ⨁ (i : ι), ↥(𝒜 i)) :
                  (a : ι) → ↥(𝒜 a))
                0) :
            A) =
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) :
                      ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ι) → ↥(𝒜 a))
                  0) :
              A) *
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) m' : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A) →
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                      ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * (m + m')) :
                    ⨁ (i : ι), ↥(𝒜 i)) :
                  (a : ι) → ↥(𝒜 a))
                0) :
            A) =
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) :
                      ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ι) → ↥(𝒜 a))
                  0) :
              A) *
            (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (m + m') : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)

Tactic:
_