-- 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 (α := ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i))
    ((decomposeAux f : (a : R[M]) → ⨁ (i : ι), ↥(gradeBy R (⇑f : (a : M) → ι) i)) (Finsupp.single m r) :
      ⨁ (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))
have refine : 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) sorry),
            map_one' := sorry, map_mul' := sorry : 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) sorry)
Tactic: refine (lift_single _ _ _).trans ?_