-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Rep k G
⊢ 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)))
have 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))
Tactic: ext