∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H) {A B : Rep k G} (f : A ⟶ B),
  (Rep.coindMap φ f).hom = ModuleCat.ofHom (((ModuleCat.Hom.hom f.hom).compLeft H).restrict ⋯)