-- 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
refine_2 :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * 0) :
              ⨁ (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)) 0 : (a : ι) → ↥(𝒜 a)) 0) : A)
refine_2₁ :
  ∀ {i_1 : ι} (m : ↥(𝒜 i_1)),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i))
                  ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * (↑m : A)) :
                ⨁ (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 : A) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)
refine_2₂ :
  ∀ (m 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)
⊢ ∀ (y : A),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) c hc) : A) * y) :
                ⨁ (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)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) 0) : A)

Tactic:
refine DirectSum.Decomposition.inductionOn 𝒜 ?_ ?_ ?_