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