∀ {k G H : Type u_1} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H)
  (s : G),
  TensorProduct.lift ((Rep.ind φ A).coinvariantsTensorMk B ∘ₗ Representation.IndV.mk φ A.ρ 1) ∘ₗ
      (((CategoryTheory.MonoidalCategory.curriedTensor (Rep k G)).obj A).obj ((Action.res (ModuleCat k) φ).obj B)).ρ s =
    TensorProduct.lift ((Rep.ind φ A).coinvariantsTensorMk B ∘ₗ Representation.IndV.mk φ A.ρ 1)