-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Rep k G
hf :
  ∀ (x : (↑X : Type u)) (x_1 : (↑Y : Type u)) (x_2 : (↑Z : Type u)),
    Eq (α := TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u))
      (((((TensorProduct.AlgebraTensorModule.curry
                      (((TensorProduct.AlgebraTensorModule.curry
                              (↑(LinearEquiv.symm (TensorProduct.assoc k (↑X : Type u) (↑Y : Type u) (↑Z : Type u)) ≪≫ₗ
                                    (TensorProduct.comm k (TensorProduct k (↑X : Type u) (↑Y : Type u))
                                        (↑Z : Type u) ≪≫ₗ
                                      LinearEquiv.symm
                                        (TensorProduct.assoc k (↑Z : Type u) (↑X : Type u) (↑Y : Type u)))) :
                                TensorProduct k (↑X : Type u) (TensorProduct k (↑Y : Type u) (↑Z : Type u)) →ₗ[k]
                                  TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u)) :
                            (↑X : Type u) →ₗ[k]
                              TensorProduct k (↑Y : Type u) (↑Z : Type u) →ₗ[k]
                                TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u)) :
                          (a : (↑X : Type u)) →
                            TensorProduct k (↑Y : Type u) (↑Z : Type u) →ₗ[k]
                              TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u))
                        x) :
                    (↑Y : Type u) →ₗ[k]
                      (↑Z : Type u) →ₗ[k] TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u)) :
                  (a : (↑Y : Type u)) →
                    (↑Z : Type u) →ₗ[k] TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u))
                x_1 :
              (↑Z : Type u) →ₗ[k] TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u)) :
            (a : (↑Z : Type u)) → TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u))
          x_2 :
        TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u))
      (((((TensorProduct.AlgebraTensorModule.curry
                      (((TensorProduct.AlgebraTensorModule.curry
                              ((LinearMap.rTensor (↑Y : Type u)
                                    (↑(TensorProduct.comm k (↑X : Type u) (↑Z : Type u)) :
                                      TensorProduct k (↑X : Type u) (↑Z : Type u) →ₗ[k]
                                        TensorProduct k (↑Z : Type u) (↑X : Type u)) ∘ₗ
                                  (↑(LinearEquiv.symm
                                        (TensorProduct.assoc k (↑X : Type u) (↑Z : Type u) (↑Y : Type u))) :
                                    TensorProduct k (↑X : Type u) (TensorProduct k (↑Z : Type u) (↑Y : Type u)) →ₗ[k]
                                      TensorProduct k (TensorProduct k (↑X : Type u) (↑Z : Type u)) (↑Y : Type u))) ∘ₗ
                                LinearMap.lTensor (↑X : Type u)
                                  (↑(TensorProduct.comm k (↑Y : Type u) (↑Z : Type u)) :
                                    TensorProduct k (↑Y : Type u) (↑Z : Type u) →ₗ[k]
                                      TensorProduct k (↑Z : Type u) (↑Y : Type u))) :
                            (↑X : Type u) →ₗ[k]
                              TensorProduct k (↑Y : Type u) (↑Z : Type u) →ₗ[k]
                                TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u)) :
                          (a : (↑X : Type u)) →
                            TensorProduct k (↑Y : Type u) (↑Z : Type u) →ₗ[k]
                              TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u))
                        x) :
                    (↑Y : Type u) →ₗ[k]
                      (↑Z : Type u) →ₗ[k] TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u)) :
                  (a : (↑Y : Type u)) →
                    (↑Z : Type u) →ₗ[k] TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u))
                x_1 :
              (↑Z : Type u) →ₗ[k] TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u)) :
            (a : (↑Z : Type u)) → TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u))
          x_2 :
        TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u))
⊢ Eq (α :=
    TensorProduct k (↑X : Type u) (TensorProduct k (↑Y : Type u) (↑Z : Type u)) →ₗ[k]
      TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u))
    (↑(LinearEquiv.symm (TensorProduct.assoc k (↑X : Type u) (↑Y : Type u) (↑Z : Type u)) ≪≫ₗ
          (TensorProduct.comm k (TensorProduct k (↑X : Type u) (↑Y : Type u)) (↑Z : Type u) ≪≫ₗ
            LinearEquiv.symm (TensorProduct.assoc k (↑Z : Type u) (↑X : Type u) (↑Y : Type u)))) :
      TensorProduct k (↑X : Type u) (TensorProduct k (↑Y : Type u) (↑Z : Type u)) →ₗ[k]
        TensorProduct k (TensorProduct k (↑Z : Type u) (↑X : Type u)) (↑Y : Type u))
    ((LinearMap.rTensor (↑Y : Type u)
          (↑(TensorProduct.comm k (↑X : Type u) (↑Z : Type u)) :
            TensorProduct k (↑X : Type u) (↑Z : Type u) →ₗ[k] TensorProduct k (↑Z : Type u) (↑X : Type u)) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.assoc k (↑X : Type u) (↑Z : Type u) (↑Y : Type u))) :
          TensorProduct k (↑X : Type u) (TensorProduct k (↑Z : Type u) (↑Y : Type u)) →ₗ[k]
            TensorProduct k (TensorProduct k (↑X : Type u) (↑Z : Type u)) (↑Y : Type u))) ∘ₗ
      LinearMap.lTensor (↑X : Type u)
        (↑(TensorProduct.comm k (↑Y : Type u) (↑Z : Type u)) :
          TensorProduct k (↑Y : Type u) (↑Z : Type u) →ₗ[k] TensorProduct k (↑Z : Type u) (↑Y : Type u)))

Tactic:
ext