{k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Monoid G] →
      (A B : Rep k G) →
        (α : Type u) →
          [DecidableEq α] →
            CategoryTheory.MonoidalCategoryStruct.tensorObj A (Rep.finsupp α B) ≅
              Rep.finsupp α (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)