-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
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
⊢ 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)
have 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)
Tactic: ext x y z