-- 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
hf :
  ∀
    (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))
⊢ 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) =
    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)

Tactic:
ext