-- 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 →+ ι
i j : Multiplicative M
e_1 :
  (↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
          ((f : (a : M) → ι)
              (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
                ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) :
            ι)) →+
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) =
    (↥(gradeBy R (⇑f : (a : M) → ι)
          (HAdd.hAdd (α := ι) (β := ι)
            ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
            ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι))) →+
      ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
e_2 :
  ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
        ((f : (a : M) → ι)
            (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
              ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) :
          ι)) =
    ↥(gradeBy R (⇑f : (a : M) → ι)
        (HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
          ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)))
e_3 :
  HEq (α :=
    outParam
      (↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
            ((f : (a : M) → ι)
                (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
                  ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) :
              ι)) →
        Type (max (max u_1 u_2) u_3)))
    fun
      (x :
        ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
            ((f : (a : M) → ι)
                (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
                  ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) :
              ι))) ↦
    ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i) (β :=
    outParam
      (↥(gradeBy R (⇑f : (a : M) → ι)
            (HAdd.hAdd (α := ι) (β := ι)
              ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
              ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι))) →
        Type (max (max u_1 u_2) u_3)))
    fun
      (x :
        ↥(gradeBy R (⇑f : (a : M) → ι)
            (HAdd.hAdd (α := ι) (β := ι)
              ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
              ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)))) ↦
    ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)
e_1_1 :
  ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
        ((f : (a : M) → ι)
            (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
              ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) :
          ι)) =
    ↥(gradeBy R (⇑f : (a : M) → ι)
        (HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
          ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)))
⊢ (f : (a : M) → ι)
      (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
        ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) =
    HAdd.hAdd (α := ι) (β := ι) ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)
      ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)

Tactic:
{ rw [map_add] }

Premises used: map_add