∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {n : ℕ} (g : G) (f : (Fin n → G) →₀ k) (r : k),
  (CategoryTheory.ConcreteCategory.hom (Rep.diagonalSuccIsoTensorTrivial k G n).inv.hom) ((fun₀ | g => r) ⊗ₜ[k] f) =
    ((Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => fun₀ | g • Fin.partialProd f => r) f