-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
k : Type u
G : Type v
V : Type u
inst : Field k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
ρV : Representation k G V
W : FDRep k G
g : G
h :
  Eq (α :=
    (↑((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V.obj (P :=
            ModuleCat.isFG k)) :
        Type u) →ₗ[k]
      (↑((of (ρV.linHom W.ρ)).V.obj (P := ModuleCat.isFG k)) : Type u))
    (ModuleCat.Hom.hom
        (InducedCategory.Hom.hom
          (CategoryStruct.comp (Y :=
            (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V)
            (((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).ρ :
                  (a : G) → End (of ρV.dual ⊗ W).V)
                g :
              End (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V)
            (Iso.hom (dualTensorIsoLinHomAux ρV W) :
              (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
                (of (ρV.linHom W.ρ)).V))) :
      (↑((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V.obj (P :=
              ModuleCat.isFG k)) :
          Type u) →ₗ[k]
        (↑((of (ρV.linHom W.ρ)).V.obj (P := ModuleCat.isFG k)) : Type u))
    (ModuleCat.Hom.hom
        (InducedCategory.Hom.hom
          (CategoryStruct.comp (Y := (of (ρV.linHom W.ρ)).V)
            (Iso.hom (dualTensorIsoLinHomAux ρV W) :
              (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
                (of (ρV.linHom W.ρ)).V)
            (((of (ρV.linHom W.ρ)).ρ : (a : G) → End (of (ρV.linHom W.ρ)).V) g : End (of (ρV.linHom W.ρ)).V))) :
      (↑((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V.obj (P :=
              ModuleCat.isFG k)) :
          Type u) →ₗ[k]
        (↑((of (ρV.linHom W.ρ)).V.obj (P := ModuleCat.isFG k)) : Type u))
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
      (of (ρV.linHom W.ρ)).V)
    (CategoryStruct.comp (Y :=
        (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V)
        (((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).ρ :
              (a : G) → End (of ρV.dual ⊗ W).V)
            g :
          End (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V)
        (Iso.hom (dualTensorIsoLinHomAux ρV W) :
          (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
            (of (ρV.linHom W.ρ)).V) :
      (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
        (of (ρV.linHom W.ρ)).V)
    (CategoryStruct.comp (Y := (of (ρV.linHom W.ρ)).V)
        (Iso.hom (dualTensorIsoLinHomAux ρV W) :
          (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
            (of (ρV.linHom W.ρ)).V)
        (((of (ρV.linHom W.ρ)).ρ : (a : G) → End (of (ρV.linHom W.ρ)).V) g : End (of (ρV.linHom W.ρ)).V) :
      (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
        (of (ρV.linHom W.ρ)).V)

Tactic:
ext : 1