-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Rep.{w, u, v} k G
f : X ⟶ Y
r : k
x :
  (↑(Functor.obj
        (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
          (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
          ModuleCat.carrier))
        X) :
    Type w)
⊢ Eq (α :=
    (↑(Functor.obj
          (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
            (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
            ModuleCat.carrier))
          Y) :
      Type w))
    ((ModuleCat.Hom.hom
            (CategoryTheory.Functor.map
              (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
                (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w))
                (CD := ModuleCat.carrier))
              (r • f)) :
          (a : (↑((forget₂ (Rep k G) (ModuleCat k)).obj X) : Type w)) →
            (↑((forget₂ (Rep k G) (ModuleCat k)).obj Y) : Type w))
        x :
      (↑(Functor.obj
            (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
              (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
              ModuleCat.carrier))
            Y) :
        Type w))
    ((ModuleCat.Hom.hom
            (HSMul.hSMul (β :=
              Functor.obj
                  (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
                    (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w))
                    (CD := ModuleCat.carrier))
                  X ⟶
                Functor.obj
                  (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
                    (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w))
                    (CD := ModuleCat.carrier))
                  Y)
              r
              (CategoryTheory.Functor.map
                (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
                  (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w))
                  (CD := ModuleCat.carrier))
                f)) :
          (a : (↑((forget₂ (Rep k G) (ModuleCat k)).obj X) : Type w)) →
            (↑((forget₂ (Rep k G) (ModuleCat k)).obj Y) : Type w))
        x :
      (↑(Functor.obj
            (forget₂ (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)
              (ModuleCat.{w, u} k) (FD := fun (x1 x2 : ModuleCat.{w, u} k) ↦ (↑x1 : Type w) →ₗ[k] (↑x2 : Type w)) (CD :=
              ModuleCat.carrier))
            Y) :
        Type w))

Tactic:
simp [smul_hom]

Premises used: Rep.smul_hom