∀ {k G H : Type u_1} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H) {A B : Rep k G}
  (f : A ⟶ B) (h : H),
  CategoryTheory.CategoryStruct.comp ((Rep.coind' φ A).ρ h)
      (ModuleCat.ofHom (CategoryTheory.Linear.rightComp k ((Action.res (ModuleCat k) φ).obj (Rep.leftRegular k H)) f)) =
    CategoryTheory.CategoryStruct.comp
      (ModuleCat.ofHom (CategoryTheory.Linear.rightComp k ((Action.res (ModuleCat k) φ).obj (Rep.leftRegular k H)) f))
      ((Rep.coind' φ B).ρ h)