-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Grading (goal)
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
h :
  ∀ (x : R[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) : ι)
h₁ :
  ↥(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) : ι)
h₂ :
  ∀ (x : R[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) : ι)
h₃ :
  (↥(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)) →
    ↥(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) : ι))) →
      (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)) →
        ↥(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) : ι)
h₄ :
  (↥(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)) →
    (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) : ι)
⊢ HMul.hMul (α := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) (β := ⨁ (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) i : M) : ι) :
              ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
                    ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι)) →+
                ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
            (a :
                ↥(gradeBy R (⇑f : (a : M) → ι)
                    ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i)))) →
              ⨁ (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) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M) : ι))
              x)
            (Finsupp.single ((Multiplicative.toAdd : (a : Multiplicative M) → M) i) 1) ⋯) :
        ⨁ (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) j : M) : ι) :
              ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
                    ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι)) →+
                ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
            (a :
                ↥(gradeBy R (⇑f : (a : M) → ι)
                    ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j)))) →
              ⨁ (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) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M) : ι))
              x)
            (Finsupp.single ((Multiplicative.toAdd : (a : Multiplicative M) → M) j) 1) ⋯) :
        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) =
    ((DirectSum.of (ι := ι) (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i))
            ((f : (a : M) → ι)
                (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
                  ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) :
              ι) :
          ↥(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)) :
        (a :
            ↥(gradeBy R (⇑f : (a : M) → ι)
                ((f : (a : M) → ι)
                  ((Multiplicative.toAdd : (a : Multiplicative M) → M) i +
                    (Multiplicative.toAdd : (a : Multiplicative M) → M) j)))) →
          ⨁ (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) → ι)
                (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
                  ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M)) :
              ι))
          x)
        (Finsupp.single
          (HAdd.hAdd (α := M) (β := M) ((Multiplicative.toAdd : (a : Multiplicative M) → M) i : M)
            ((Multiplicative.toAdd : (a : Multiplicative M) → M) j : M))
          1)
        ⋯)
have h₅ : ↥(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) : ι))) →
  ∀ (x : R[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: convert! DirectSum.of_mul_of (A := (fun i : ι => gradeBy R f i)) _ _