-- Lean 4 proof step from Mathlib.RepresentationTheory.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : Monoid G
M : Type u_4
inst_2 : AddCommMonoid M
inst_3 : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
hM :
  ∀ (m_1 : G),
    Eq (α := RestrictScalars k k[G] M)
      ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) ((of k G : (a : G) → k[G]) m_1) :
              End k (RestrictScalars k k[G] M)) :
            (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
          m :
        RestrictScalars k k[G] M)
      ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] M) : (a : M) → RestrictScalars k k[G] M)
          (HSMul.hSMul (α := k[G]) (β := M) ((of k G : (a : G) → k[G]) m_1 : k[G])
            ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
        RestrictScalars k k[G] M)
hadd :
  ∀ (x y : k[G]),
    Eq (α := RestrictScalars k k[G] M)
        ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) x :
                End k (RestrictScalars k k[G] M)) :
              (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
            m :
          RestrictScalars k k[G] M)
        ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] M) : (a : M) → RestrictScalars k k[G] M)
            (HSMul.hSMul (β := M) x ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
          RestrictScalars k k[G] M) →
      Eq (α := RestrictScalars k k[G] M)
          ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) y :
                  End k (RestrictScalars k k[G] M)) :
                (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
              m :
            RestrictScalars k k[G] M)
          ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] M) : (a : M) → RestrictScalars k k[G] M)
              (HSMul.hSMul (β := M) y
                ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
            RestrictScalars k k[G] M) →
        Eq (α := RestrictScalars k k[G] M)
          ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) (x + y) :
                  End k (RestrictScalars k k[G] M)) :
                (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
              m :
            RestrictScalars k k[G] M)
          ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] M) : (a : M) → RestrictScalars k k[G] M)
              (HSMul.hSMul (β := M) (x + y)
                ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
            RestrictScalars k k[G] M)
⊢ Eq (α := RestrictScalars k k[G] M)
    ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) r :
            End k (RestrictScalars k k[G] M)) :
          (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
        m :
      RestrictScalars k k[G] M)
    ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] M) : (a : M) → RestrictScalars k k[G] M)
        (HSMul.hSMul (β := M) r ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
      RestrictScalars k k[G] M)
have hsmul : ∀ (r : k) (x : k[G]),
  Eq (α := RestrictScalars k k[G] M)
      ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) x :
              End k (RestrictScalars k k[G] M)) :
            (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
          m :
        RestrictScalars k k[G] M)
      ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] M) : (a : M) → RestrictScalars k k[G] M)
          (HSMul.hSMul (β := M) x ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
        RestrictScalars k k[G] M) →
    Eq (α := RestrictScalars k k[G] M)
      ((((asAlgebraHom (ofModule M) : (a : k[G]) → End k (RestrictScalars k k[G] M)) (r • x) :
              End k (RestrictScalars k k[G] M)) :
            (a : RestrictScalars k k[G] M) → RestrictScalars k k[G] M)
          m :
        RestrictScalars k k[G] M)
      ((AddEquiv.symm (RestrictScalars.addEquiv k k[G] M) : (a : M) → RestrictScalars k k[G] M)
          (HSMul.hSMul (β := M) (r • x)
            ((RestrictScalars.addEquiv k k[G] M : (a : RestrictScalars k k[G] M) → M) m : M)) :
        RestrictScalars k k[G] M)
Tactic: apply MonoidAlgebra.induction_on r