∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H),
  Rep.coinvariantsTensorIndHom φ A B =
    ModuleCat.ofHom
      (Representation.Coinvariants.lift
        (((CategoryTheory.MonoidalCategory.curriedTensor (Rep k H)).obj (Rep.ind φ A)).obj B).ρ
        (TensorProduct.lift
          (Representation.Coinvariants.lift
            (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
            (TensorProduct.lift
              ((Finsupp.lift
                  (↑A.V →ₗ[k]
                    ↑(((Action.functorCategoryEquivalence (ModuleCat k) H).symm.inverse.obj B).obj PUnit.unit) →ₗ[k]
                      (((CategoryTheory.MonoidalCategory.curriedTensor (Rep k G)).obj A).obj
                            ((Action.res (ModuleCat k) φ).obj B)).ρ.Coinvariants)
                  k H)
                fun g => (A.coinvariantsTensorMk ((Action.res (ModuleCat k) φ).obj B)).compl₂ (B.ρ g)))
            ⋯))
        ⋯)