∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep k G) (α : Type u) [inst_2 : DecidableEq α],
  A.finsuppToCoinvariantsTensorFree α =
    ModuleCat.Hom.hom ((Rep.coinvariantsFunctor k G).map (A.finsuppTensorRight (Rep.leftRegular k G) α).inv) ∘ₗ
      ↑(((A.ρ.tprod (Representation.leftRegular k G)).coinvariantsFinsuppLEquiv α).trans
            (Finsupp.lcongr (Equiv.refl α) A.ρ.coinvariantsTprodLeftRegularLEquiv)).symm