-- Lean 4 proof step from Mathlib.RepresentationTheory.Intertwining (goal)
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
⊢ Eq (α := TensorProduct A (TensorProduct A V W) U →ₗ[A] TensorProduct A V (TensorProduct A W U))
    ((↑(_root_.TensorProduct.assoc A V W U) :
        TensorProduct A (TensorProduct A V W) U →ₗ[A] TensorProduct A V (TensorProduct A W U)) ∘ₗ
      ((ρ.tprod σ).tprod τ :
          (a : G) → TensorProduct A (TensorProduct A V W) U →ₗ[A] TensorProduct A (TensorProduct A V W) U)
        g)
    ((ρ.tprod (σ.tprod τ) :
          (a : G) → TensorProduct A V (TensorProduct A W U) →ₗ[A] TensorProduct A V (TensorProduct A W U))
        g ∘ₗ
      (↑(_root_.TensorProduct.assoc A V W U) :
        TensorProduct A (TensorProduct A V W) U →ₗ[A] TensorProduct A V (TensorProduct A W U)))
have a : ∀ (x : V) (x_1 : W) (x_2 : U),
  Eq (α := TensorProduct A V (TensorProduct A W U))
    (((((((TensorProduct.AlgebraTensorModule.curry
                          (TensorProduct.AlgebraTensorModule.curry
                            ((↑(_root_.TensorProduct.assoc A V W U) :
                                TensorProduct A (TensorProduct A V W) U →ₗ[A]
                                  TensorProduct A V (TensorProduct A W U)) ∘ₗ
                              ((ρ.tprod σ).tprod τ :
                                  (a : G) →
                                    TensorProduct A (TensorProduct A V W) U →ₗ[A]
                                      TensorProduct A (TensorProduct A V W) U)
                                g)) :
                        V →ₗ[A] W →ₗ[A] U →ₗ[A] TensorProduct A V (TensorProduct A W U)) :
                      (a : V) → W →ₗ[A] U →ₗ[A] TensorProduct A V (TensorProduct A W U))
                    x :
                  W →ₗ[A] U →ₗ[A] TensorProduct A V (TensorProduct A W U)) :
                (a : W) → U →ₗ[A] TensorProduct A V (TensorProduct A W U))
              x_1 :
            U →ₗ[A] TensorProduct A V (TensorProduct A W U)) :
          (a : U) → TensorProduct A V (TensorProduct A W U))
        x_2 :
      TensorProduct A V (TensorProduct A W U))
    (((((((TensorProduct.AlgebraTensorModule.curry
                          (TensorProduct.AlgebraTensorModule.curry
                            ((ρ.tprod (σ.tprod τ) :
                                  (a : G) →
                                    TensorProduct A V (TensorProduct A W U) →ₗ[A]
                                      TensorProduct A V (TensorProduct A W U))
                                g ∘ₗ
                              (↑(_root_.TensorProduct.assoc A V W U) :
                                TensorProduct A (TensorProduct A V W) U →ₗ[A]
                                  TensorProduct A V (TensorProduct A W U)))) :
                        V →ₗ[A] W →ₗ[A] U →ₗ[A] TensorProduct A V (TensorProduct A W U)) :
                      (a : V) → W →ₗ[A] U →ₗ[A] TensorProduct A V (TensorProduct A W U))
                    x :
                  W →ₗ[A] U →ₗ[A] TensorProduct A V (TensorProduct A W U)) :
                (a : W) → U →ₗ[A] TensorProduct A V (TensorProduct A W U))
              x_1 :
            U →ₗ[A] TensorProduct A V (TensorProduct A W U)) :
          (a : U) → TensorProduct A V (TensorProduct A W U))
        x_2 :
      TensorProduct A V (TensorProduct A W U))
Tactic: ext