-- Module: Mathlib.RepresentationTheory.Equiv
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
inst_12 : DecidableEq α
g : G
a :
  ∀ (x : V) (a : α) (x_1 : W) (a_1 : α),
    Eq (α := TensorProduct k V W)
      ((((((TensorProduct.AlgebraTensorModule.curry
                            (((↑(TensorProduct.finsuppRight k k V W α) :
                                  TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W) :
                                TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W) ∘ₗ
                              ((σ.tprod (ρ.finsupp α) :
                                    (a : G) → TensorProduct k V (α →₀ W) →ₗ[k] TensorProduct k V (α →₀ W))
                                  g :
                                TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] TensorProduct.{u, v', w'} k V (α →₀ W))) :
                          V →ₗ[k] (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W) :
                        (a : V) → (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W)
                      x ∘ₗ
                    lsingle a :
                  (a : W) → α →₀ TensorProduct k V W)
                x_1 :
              α →₀ TensorProduct k V W) :
            (a : α) → TensorProduct k V W)
          a_1 :
        TensorProduct k V W)
      ((((((TensorProduct.AlgebraTensorModule.curry
                            ((((σ.tprod ρ).finsupp α :
                                    (a : G) → (α →₀ TensorProduct k V W) →ₗ[k] α →₀ TensorProduct k V W)
                                  g :
                                (α →₀ TensorProduct k V W) →ₗ[k] α →₀ TensorProduct k V W) ∘ₗ
                              ((↑(TensorProduct.finsuppRight k k V W α) :
                                  TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W) :
                                TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W)) :
                          V →ₗ[k] (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W) :
                        (a : V) → (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W)
                      x ∘ₗ
                    lsingle a :
                  (a : W) → α →₀ TensorProduct k V W)
                x_1 :
              α →₀ TensorProduct k V W) :
            (a : α) → TensorProduct k V W)
          a_1 :
        TensorProduct k V W)
⊢ Eq (α := TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W)
    (((↑(TensorProduct.finsuppRight k k V W α) :
            TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W) :
          TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W) ∘ₗ
        ((σ.tprod (ρ.finsupp α) : (a : G) → TensorProduct k V (α →₀ W) →ₗ[k] TensorProduct k V (α →₀ W)) g :
          TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] TensorProduct.{u, v', w'} k V (α →₀ W)) :
      TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W)
    ((((σ.tprod ρ).finsupp α : (a : G) → (α →₀ TensorProduct k V W) →ₗ[k] α →₀ TensorProduct k V W) g :
          (α →₀ TensorProduct k V W) →ₗ[k] α →₀ TensorProduct k V W) ∘ₗ
        ((↑(TensorProduct.finsuppRight k k V W α) :
            TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W) :
          TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W) :
      TensorProduct.{u, v', w'} k V (α →₀ W) →ₗ[k] α →₀ TensorProduct k V W)

Tactic:
ext