-- Lean 4 proof step from Mathlib.RepresentationTheory.Action (goal)
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 : X.V
a_1 : Y.V
a_2 : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V
⊢ 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 :
                      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_1 :
              (a : k) → (X ⊗ Y).V →₀ k)
            1 :
          (a : (X ⊗ Y).V) → k)
        a_2 :
      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 :
                      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_1 :
              (a : k) → (X ⊗ Y).V →₀ k)
            1 :
          (a : (X ⊗ Y).V) → k)
        a_2 :
      k)
have 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,
              (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((Y.ρ : (a : G) → End Y.V) g) : (a : Y.V) → Y.V) a_1)
            1 :
          Finsupp.{w, u} (X.V × Y.V) k) :
        (a : X.V × Y.V) → k)
      a_2 :
    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, a_1))
            1 :
          Finsupp.{w, u} (X.V × Y.V) k) :
        (a : X.V × Y.V) → k)
      a_2 :
    k)
Tactic: simp [linearize_single _]