-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : DecidableEq ι
inst_2 : AddMonoid ι
inst_3 : CommSemiring R
f : M →+ ι
m : M
r : R
h :
  Eq (α := GradedMonoid fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i))
    (GradedMonoid.mk (A := fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i))
        ((f : (a : M) → ι)
          ((Multiplicative.toAdd : (a : Multiplicative M) → M)
              ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M) :
            M))
        (HSMul.hSMul (β :=
          ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
              ((f : (a : M) → ι)
                  ((Multiplicative.toAdd : (a : Multiplicative M) → M)
                      ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M) :
                    M) :
                ι)))
          r
          (Subtype.mk (p := fun (x : R[M]) ↦
              Membership.mem (γ := Submodule R R[M])
                (gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
                  ((f : (a : M) → ι)
                      ((Multiplicative.toAdd : (a : Multiplicative M) → M)
                          ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M) :
                        M) :
                    ι))
                x)
              (Finsupp.single
                ((Multiplicative.toAdd : (a : Multiplicative M) → M)
                  ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M))
                1)
              ⋯ :
            ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
                ((f : (a : M) → ι)
                    ((Multiplicative.toAdd : (a : Multiplicative M) → M)
                        ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M) :
                      M) :
                  ι)))) :
      GradedMonoid fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i))
    (GradedMonoid.mk (A := fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) ((f : (a : M) → ι) m)
        (Subtype.mk (p := fun (x : R[M]) ↦
          Membership.mem (γ := Submodule R R[M])
            (gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι) ((f : (a : M) → ι) m : ι)) x)
          (Finsupp.single m r) ⋯) :
      GradedMonoid fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i))
⊢ Eq (α := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
    (((DirectSum.of (ι := ι) (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i))
              ((f : (a : M) → ι)
                  ((Multiplicative.toAdd : (a : Multiplicative M) → M)
                      ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M) :
                    M) :
                ι) :
            ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
                  ((f : (a : M) → ι)
                      ((Multiplicative.toAdd : (a : Multiplicative M) → M)
                          ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M) :
                        M) :
                    ι)) →+
              ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
          (a :
              ↥(gradeBy R (⇑f : (a : M) → ι)
                  ((f : (a : M) → ι)
                    ((Multiplicative.toAdd : (a : Multiplicative M) → M)
                      ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m))))) →
            ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
        (HSMul.hSMul (β :=
          ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
              ((f : (a : M) → ι)
                  ((Multiplicative.toAdd : (a : Multiplicative M) → M)
                      ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M) :
                    M) :
                ι)))
          r
          (Subtype.mk (p := fun (x : R[M]) ↦
              Membership.mem (γ := Submodule R R[M])
                (gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
                  ((f : (a : M) → ι)
                      ((Multiplicative.toAdd : (a : Multiplicative M) → M)
                          ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M) :
                        M) :
                    ι))
                x)
              (Finsupp.single
                ((Multiplicative.toAdd : (a : Multiplicative M) → M)
                  ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M))
                1)
              ⋯ :
            ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
                ((f : (a : M) → ι)
                    ((Multiplicative.toAdd : (a : Multiplicative M) → M)
                        ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M) :
                      M) :
                  ι)))) :
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
    (((DirectSum.of (ι := ι) (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i)) ((f : (a : M) → ι) m : ι) :
            ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι) ((f : (a : M) → ι) m : ι)) →+
              ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
          (a : ↥(gradeBy R (⇑f : (a : M) → ι) ((f : (a : M) → ι) m))) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
        (Subtype.mk (p := fun (x : R[M]) ↦
          Membership.mem (γ := Submodule R R[M])
            (gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι) ((f : (a : M) → ι) m : ι)) x)
          (Finsupp.single m r) ⋯) :
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))

Tactic:
apply DirectSum.of_eq_of_gradedMonoid_eq

Premises used: DirectSum.of_eq_of_gradedMonoid_eq