-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → NonUnitalSemiring (A i)
inst_2 : (i : ι) → Module.{u_3, u_4} R (A i)
inst_3 : ∀ (i : ι), SMulCommClass.{u_3, u_4, u_4} R (A i) (A i)
inst_4 : ∀ (i : ι), IsScalarTower.{u_3, u_4, u_4} R (A i) (A i)
x y z : ⨂[R] (i : ι), A i
H :
  ∀ (x y z : (i : ι) → A i),
    Eq (α := ⨂[R] (i : ι), A i)
      ((LinearMap.compMultilinearMap (M₁ := A)
              ((LinearMap.compMultilinearMap (M₁ := A)
                    ((LinearMap.compMultilinearMap (M₁ := A)
                          ((LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i)
                                  ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
                                (a : (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →
                                  ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →ₗ[R]
                                    (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
                              (mul (A := A)) ∘ₗ
                            mul (A := A))
                          (tprod R (s := A)) :
                        (a : (i : ι) → A i) → (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
                      x)
                    (tprod R (s := A)) :
                  (a : (i : ι) → A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
                y)
              (tprod R (s := A)) :
            (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
          z :
        ⨂[R] (i : ι), A i)
      ((LinearMap.compMultilinearMap (M₁ := A)
              ((LinearMap.compMultilinearMap (M₁ := A)
                    (((LinearMap.compMultilinearMap (M₁ := A)
                            (LinearMap.flip
                              ((((LinearMap.llcomp R (⨂[R] (i : ι), A i)
                                          ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
                                          ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
                                        (a :
                                            ((⨂[R] (i : ι), A i) →ₗ[R]
                                                (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →ₗ[R]
                                              (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →
                                          ((⨂[R] (i : ι), A i) →ₗ[R]
                                              (⨂[R] (i : ι), A i) →ₗ[R]
                                                (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →ₗ[R]
                                            (⨂[R] (i : ι), A i) →ₗ[R]
                                              (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
                                      (↑LinearMap.lflip :
                                        ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →ₗ[R]
                                          (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
                                    ((⨂[R] (i : ι), A i) →ₗ[R]
                                        (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →ₗ[R]
                                      (⨂[R] (i : ι), A i) →ₗ[R]
                                        (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
                                  (a :
                                      (⨂[R] (i : ι), A i) →ₗ[R]
                                        (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →
                                    (⨂[R] (i : ι), A i) →ₗ[R]
                                      (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
                                ((LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i)
                                        ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
                                      (a : (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →
                                        ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →ₗ[R]
                                          (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
                                    (LinearMap.flip (mul (A := A))) ∘ₗ
                                  mul (A := A))))
                            (tprod R (s := A)) :
                          MultilinearMap R A ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)) :
                        (a : (i : ι) → A i) → (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
                      x)
                    (tprod R (s := A)) :
                  (a : (i : ι) → A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
                y)
              (tprod R (s := A)) :
            (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
          z :
        ⨂[R] (i : ι), A i)
⊢ Eq (α := (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
    ((LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
            (a : (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →
              ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →ₗ[R]
                (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
          (mul (A := A)) ∘ₗ
        mul (A := A) :
      (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
    (LinearMap.flip
        ((((LinearMap.llcomp R (⨂[R] (i : ι), A i)
                    ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
                    ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
                  (a :
                      ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →ₗ[R]
                        (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →
                    ((⨂[R] (i : ι), A i) →ₗ[R]
                        (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →ₗ[R]
                      (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
                (↑LinearMap.lflip :
                  ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →ₗ[R]
                    (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
              ((⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →ₗ[R]
                (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
            (a : (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →
              (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
          ((LinearMap.llcomp R (⨂[R] (i : ι), A i) (⨂[R] (i : ι), A i) ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
                (a : (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →
                  ((⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) →ₗ[R]
                    (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
              (LinearMap.flip (mul (A := A))) ∘ₗ
            mul (A := A))) :
      (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)

Tactic:
ext x y z