∀ (k G : Type u_1) [inst : CommRing k] [inst_1 : Group G] (X : Rep k G),
  ModuleCat.ofHom
      (LinearMap.codRestrict X.ρ.invariants
        (ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.id X).hom ∘ₗ X.ρ.invariants.subtype) ⋯) =
    CategoryTheory.CategoryStruct.id (ModuleCat.of k ↥X.ρ.invariants)