-- 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 →+ ι
m : M
r : R
⊢ HSMul.hSMul (β := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) r
      (({
              toFun := fun (m : Multiplicative M) ↦
                ((DirectSum.of (ι := ι) (fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i))
                        ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) m : M) : ι) :
                      ↥(gradeBy.{u_1, u_2, u_3} (ι := ι) R ((⇑f : (a : M) → ι) : (a : M) → ι)
                            ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) m : M) : ι)) →+
                        ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) :
                    (a :
                        ↥(gradeBy R (⇑f : (a : M) → ι)
                            ((f : (a : M) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → 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) → ι) ((Multiplicative.toAdd : (a : Multiplicative M) → M) m : M) : ι))
                      x)
                    (Finsupp.single ((Multiplicative.toAdd : (a : Multiplicative M) → M) m) 1) ⋯),
              map_one' := ⋯, map_mul' := ⋯ : Multiplicative M →* ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i) } :
            (a : Multiplicative M) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
          ((Multiplicative.ofAdd : (a : 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) ⋯)
have refine : 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)
            sorry :
          ↥(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) sorry) :
    ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
Tactic: refine (DirectSum.of_smul R _ _ _).symm.trans ?_