∀ {k G V : Type u_1} [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),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj (FDRep.of ρV.dual) W).ρ g)
      (FDRep.dualTensorIsoLinHomAux ρV W).hom =
    CategoryTheory.CategoryStruct.comp (FDRep.dualTensorIsoLinHomAux ρV W).hom ((FDRep.of (ρV.linHom W.ρ)).ρ g)