-- 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
⊢ Eq (α := R[M])
    (↑(Sigma.snd (α := ι) (β := fun (a : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) a))
          (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))) :
      R[M])
    (↑(Sigma.snd (α := ι) (β := fun (a : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) a))
          (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))) :
      R[M])
have h : Eq (α := R[M])
  (single
      ((Multiplicative.toAdd : (a : Multiplicative M) → M)
        ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M))
      (r * 1) :
    R[M])
  ((↑(Sigma.snd (α := ι) (β := fun (a : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) a))
          (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) sorry) :
            GradedMonoid fun (i : ι) ↦ ↥(gradeBy R (⇑f : (a : M) → ι) i))) :
      R[M]) :
    R[M])
Tactic: refine (smul_single' _ _ _).trans ?_