-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Ring k
inst_1 : Monoid G
A B C X Y : Rep.{w, u, v} k G
f g : X ⟶ Y
hf :
  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))
        (f + g)) =
    ModuleCat.Hom.hom
      (HAdd.hAdd (α :=
        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)
        (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)
        (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))
          g))
⊢ 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 + g) =
    HAdd.hAdd (α :=
      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)
      (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)
      (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))
        g)

Tactic:
ext1