-- 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 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)
have 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)
Tactic: ext