-- Lean 4 proof step from Mathlib.RepresentationTheory.Equiv (goal)
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
⊢ 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)
have 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)
Tactic: ext