-- 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 :
  ∀ (a : α) (x : V) (x_1 : W) (a_1 : α),
    Eq (α := TensorProduct k V W)
      (((((((TensorProduct.AlgebraTensorModule.curry
                              (((↑(TensorProduct.finsuppLeft k k V W α) :
                                    TensorProduct k (α →₀ V) W →ₗ[k] α →₀ TensorProduct k V W) :
                                  TensorProduct k (α →₀ V) W →ₗ[k] α →₀ TensorProduct k V W) ∘ₗ
                                (((σ.finsupp α).tprod ρ :
                                      (a : G) → TensorProduct k (α →₀ V) W →ₗ[k] TensorProduct k (α →₀ V) W)
                                    g :
                                  TensorProduct k (α →₀ V) W →ₗ[k] TensorProduct k (α →₀ V) W)) ∘ₗ
                            lsingle a :
                          V →ₗ[k] W →ₗ[k] α →₀ TensorProduct k V W) :
                        (a : V) → W →ₗ[k] α →₀ TensorProduct k V W)
                      x :
                    W →ₗ[k] α →₀ TensorProduct k V W) :
                  (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.finsuppLeft k k V W α) :
                                    TensorProduct k (α →₀ V) W →ₗ[k] α →₀ TensorProduct k V W) :
                                  TensorProduct k (α →₀ V) W →ₗ[k] α →₀ TensorProduct k V W)) ∘ₗ
                            lsingle a :
                          V →ₗ[k] W →ₗ[k] α →₀ TensorProduct k V W) :
                        (a : V) → W →ₗ[k] α →₀ TensorProduct k V W)
                      x :
                    W →ₗ[k] α →₀ TensorProduct k V W) :
                  (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 k (α →₀ V) W →ₗ[k] α →₀ TensorProduct k V W)
    (((↑(TensorProduct.finsuppLeft k k V W α) : TensorProduct k (α →₀ V) W →ₗ[k] α →₀ TensorProduct k V W) :
          TensorProduct k (α →₀ V) W →ₗ[k] α →₀ TensorProduct k V W) ∘ₗ
        (((σ.finsupp α).tprod ρ : (a : G) → TensorProduct k (α →₀ V) W →ₗ[k] TensorProduct k (α →₀ V) W) g :
          TensorProduct k (α →₀ V) W →ₗ[k] TensorProduct k (α →₀ V) W) :
      TensorProduct 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.finsuppLeft k k V W α) : TensorProduct k (α →₀ V) W →ₗ[k] α →₀ TensorProduct k V W) :
          TensorProduct k (α →₀ V) W →ₗ[k] α →₀ TensorProduct k V W) :
      TensorProduct k (α →₀ V) W →ₗ[k] α →₀ TensorProduct k V W)

Tactic:
ext