-- Module: Mathlib.RepresentationTheory.Action
Goal:
k_1 : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k_1
inst_2 : AddCommGroup V
inst_3 : Module k_1 V
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
σ_1 : Representation k_1 G V
ρ_1 : Representation k_1 G W
X Y Z : Action (Type w) G
k : Type u
inst_6 : CommSemiring k
inst_7 : Module k V
inst_8 : Module k W
σ : Representation k G V
ρ : Representation k G W
g : G
a_1 : X.V
a_2 : Y.V
a_3 : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V
a :
  Eq.{u + 1} (α := k)
    (((Finsupp.single
              ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g) : (a : X.V) → X.V)
                  a_1,
                (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((Y.ρ : (a : G) → End Y.V) g) : (a : Y.V) → Y.V)
                  a_2)
              1 :
            Finsupp.{w, u} (X.V × Y.V) k) :
          (a : X.V × Y.V) → k)
        a_3 :
      k)
    (((Finsupp.single
              ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                    (((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).ρ : (a : G) → End (X.V × Y.V))
                      g) :
                  (a : X.V × Y.V) → X.V × Y.V)
                (a_1, a_2))
              1 :
            Finsupp.{w, u} (X.V × Y.V) k) :
          (a : X.V × Y.V) → k)
        a_3 :
      k)
⊢ Eq.{u + 1} (α := k)
    (((((TensorProduct.AlgebraTensorModule.curry
                          ((↑(finsuppTensorFinsupp' k X.V Y.V) :
                              TensorProduct k (X.V →₀ k) (Y.V →₀ k) →ₗ[k] X.V × Y.V →₀ k) ∘ₗ
                            (tprod (linearize k G X) (linearize k G Y) :
                                (a : G) →
                                  TensorProduct k (X.V →₀ k) (Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k))
                              g) ∘ₗ
                        Finsupp.lsingle a_1 :
                      k →ₗ[k]
                        Finsupp.{w, u} Y.V k →ₗ[k]
                          Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k) :
                    (a : k) → (Y.V →₀ k) →ₗ[k] (X ⊗ Y).V →₀ k)
                  1 ∘ₗ
                Finsupp.lsingle a_2 :
              (a : k) → (X ⊗ Y).V →₀ k)
            1 :
          (a : (X ⊗ Y).V) → k)
        a_3 :
      k)
    (((((TensorProduct.AlgebraTensorModule.curry
                          ((linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y) :
                                (a : G) → ((X ⊗ Y).V →₀ k) →ₗ[k] (X ⊗ Y).V →₀ k)
                              g ∘ₗ
                            (↑(finsuppTensorFinsupp' k X.V Y.V) :
                              TensorProduct k (X.V →₀ k) (Y.V →₀ k) →ₗ[k] X.V × Y.V →₀ k)) ∘ₗ
                        Finsupp.lsingle a_1 :
                      k →ₗ[k]
                        Finsupp.{w, u} Y.V k →ₗ[k]
                          Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k) :
                    (a : k) → (Y.V →₀ k) →ₗ[k] (X ⊗ Y).V →₀ k)
                  1 ∘ₗ
                Finsupp.lsingle a_2 :
              (a : k) → (X ⊗ Y).V →₀ k)
            1 :
          (a : (X ⊗ Y).V) → k)
        a_3 :
      k)

Tactic:
simp [linearize_single _]

Premises used: Representation.linearize_single