-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Iso (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Monoid G
V : Type u_3
W : Type u_4
inst_2 : AddCommGroup V
inst_3 : AddCommGroup W
inst_4 : Module k V
inst_5 : Module k W
ρ : MonoidHom.{u_2, u_3} G (V →ₗ[k] V)
σ : MonoidHom.{u_2, u_4} G (W →ₗ[k] W)
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) g = (σ : (a : G) → W →ₗ[k] W) g ∘ₗ f
r : k[G]
x : V
hM :
  ∀ (m : G),
    Eq (α := W)
      ((f : (a : V) → W)
          ((((((lift k (V →ₗ[k] V) G : (a : G →* V →ₗ[k] V) → k[G] →ₐ[k] V →ₗ[k] V) ρ : k[G] →ₐ[k] V →ₗ[k] V) :
                      (a : k[G]) → V →ₗ[k] V)
                    ((MonoidAlgebra.of k G : (a : G) → k[G]) m) :
                  V →ₗ[k] V) :
                (a : V) → V)
              x :
            V) :
        W)
      ((((((lift k (W →ₗ[k] W) G : (a : G →* W →ₗ[k] W) → k[G] →ₐ[k] W →ₗ[k] W) σ : k[G] →ₐ[k] W →ₗ[k] W) :
                  (a : k[G]) → W →ₗ[k] W)
                ((MonoidAlgebra.of k G : (a : G) → k[G]) m) :
              W →ₗ[k] W) :
            (a : W) → W)
          ((f : (a : V) → W) x : W) :
        W)
hadd :
  ∀ (x_1 y : k[G]),
    Eq (α := W)
        ((f : (a : V) → W)
            ((((((lift k (V →ₗ[k] V) G : (a : G →* V →ₗ[k] V) → k[G] →ₐ[k] V →ₗ[k] V) ρ : k[G] →ₐ[k] V →ₗ[k] V) :
                        (a : k[G]) → V →ₗ[k] V)
                      x_1 :
                    V →ₗ[k] V) :
                  (a : V) → V)
                x :
              V) :
          W)
        ((((((lift k (W →ₗ[k] W) G : (a : G →* W →ₗ[k] W) → k[G] →ₐ[k] W →ₗ[k] W) σ : k[G] →ₐ[k] W →ₗ[k] W) :
                    (a : k[G]) → W →ₗ[k] W)
                  x_1 :
                W →ₗ[k] W) :
              (a : W) → W)
            ((f : (a : V) → W) x : W) :
          W) →
      Eq (α := W)
          ((f : (a : V) → W)
              ((((((lift k (V →ₗ[k] V) G : (a : G →* V →ₗ[k] V) → k[G] →ₐ[k] V →ₗ[k] V) ρ : k[G] →ₐ[k] V →ₗ[k] V) :
                          (a : k[G]) → V →ₗ[k] V)
                        y :
                      V →ₗ[k] V) :
                    (a : V) → V)
                  x :
                V) :
            W)
          ((((((lift k (W →ₗ[k] W) G : (a : G →* W →ₗ[k] W) → k[G] →ₐ[k] W →ₗ[k] W) σ : k[G] →ₐ[k] W →ₗ[k] W) :
                      (a : k[G]) → W →ₗ[k] W)
                    y :
                  W →ₗ[k] W) :
                (a : W) → W)
              ((f : (a : V) → W) x : W) :
            W) →
        Eq (α := W)
          ((f : (a : V) → W)
              ((((((lift k (V →ₗ[k] V) G : (a : G →* V →ₗ[k] V) → k[G] →ₐ[k] V →ₗ[k] V) ρ : k[G] →ₐ[k] V →ₗ[k] V) :
                          (a : k[G]) → V →ₗ[k] V)
                        (x_1 + y) :
                      V →ₗ[k] V) :
                    (a : V) → V)
                  x :
                V) :
            W)
          ((((((lift k (W →ₗ[k] W) G : (a : G →* W →ₗ[k] W) → k[G] →ₐ[k] W →ₗ[k] W) σ : k[G] →ₐ[k] W →ₗ[k] W) :
                      (a : k[G]) → W →ₗ[k] W)
                    (x_1 + y) :
                  W →ₗ[k] W) :
                (a : W) → W)
              ((f : (a : V) → W) x : W) :
            W)
⊢ Eq (α := W)
    ((f : (a : V) → W)
        ((((((lift k (V →ₗ[k] V) G : (a : G →* V →ₗ[k] V) → k[G] →ₐ[k] V →ₗ[k] V) ρ : k[G] →ₐ[k] V →ₗ[k] V) :
                    (a : k[G]) → V →ₗ[k] V)
                  r :
                V →ₗ[k] V) :
              (a : V) → V)
            x :
          V) :
      W)
    ((((((lift k (W →ₗ[k] W) G : (a : G →* W →ₗ[k] W) → k[G] →ₐ[k] W →ₗ[k] W) σ : k[G] →ₐ[k] W →ₗ[k] W) :
                (a : k[G]) → W →ₗ[k] W)
              r :
            W →ₗ[k] W) :
          (a : W) → W)
        ((f : (a : V) → W) x : W) :
      W)
have hsmul : ∀ (r : k) (x_1 : k[G]),
  Eq (α := W)
      ((f : (a : V) → W)
          ((((((lift k (V →ₗ[k] V) G : (a : G →* V →ₗ[k] V) → k[G] →ₐ[k] V →ₗ[k] V) ρ : k[G] →ₐ[k] V →ₗ[k] V) :
                      (a : k[G]) → V →ₗ[k] V)
                    x_1 :
                  V →ₗ[k] V) :
                (a : V) → V)
              x :
            V) :
        W)
      ((((((lift k (W →ₗ[k] W) G : (a : G →* W →ₗ[k] W) → k[G] →ₐ[k] W →ₗ[k] W) σ : k[G] →ₐ[k] W →ₗ[k] W) :
                  (a : k[G]) → W →ₗ[k] W)
                x_1 :
              W →ₗ[k] W) :
            (a : W) → W)
          ((f : (a : V) → W) x : W) :
        W) →
    Eq (α := W)
      ((f : (a : V) → W)
          ((((((lift k (V →ₗ[k] V) G : (a : G →* V →ₗ[k] V) → k[G] →ₐ[k] V →ₗ[k] V) ρ : k[G] →ₐ[k] V →ₗ[k] V) :
                      (a : k[G]) → V →ₗ[k] V)
                    (r • x_1) :
                  V →ₗ[k] V) :
                (a : V) → V)
              x :
            V) :
        W)
      ((((((lift k (W →ₗ[k] W) G : (a : G →* W →ₗ[k] W) → k[G] →ₐ[k] W →ₗ[k] W) σ : k[G] →ₐ[k] W →ₗ[k] W) :
                  (a : k[G]) → W →ₗ[k] W)
                (r • x_1) :
              W →ₗ[k] W) :
            (a : W) → W)
          ((f : (a : V) → W) x : W) :
        W)
Tactic: apply MonoidAlgebra.induction_on r