-- 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 :
  ∀ (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)
⊢ Eq (α :=
    TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k) →ₗ[k]
      Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k)
    ((↑(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)
    ((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))

Tactic:
ext