-- Module: Mathlib.RepresentationTheory.Intertwining
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
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))
⊢ 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)))

Tactic:
ext