∀ (k G : Type u_1) [inst : CommRing k] [inst_1 : Group G] (g : G),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxMonoidal.ε (TannakaDuality.FiniteGroup.forget k G).toFunctor)
      (TannakaDuality.FiniteGroup.equivApp g (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FDRep k G))).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxMonoidal.ε (TannakaDuality.FiniteGroup.forget k G).toFunctor)
      (TannakaDuality.FiniteGroup.equivApp g (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FDRep k G))).hom