∀ (k : Type u_1) {G H : Type u_1} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  {X' X : Rep k G} {Y : Rep k H} (x : X' ⟶ X) (x_1 : X ⟶ (Action.res (ModuleCat k) φ).obj Y) (x_2 : H),
  ModuleCat.Hom.hom ((Rep.indResHomEquiv φ X' Y).toEquiv.symm (CategoryTheory.CategoryStruct.comp x x_1)).hom ∘ₗ
      Representation.IndV.mk φ X'.ρ x_2 =
    ModuleCat.Hom.hom
        (CategoryTheory.CategoryStruct.comp ((Rep.indFunctor k φ).map x)
            ((Rep.indResHomEquiv φ X Y).toEquiv.symm x_1)).hom ∘ₗ
      Representation.IndV.mk φ X'.ρ x_2