-- 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
suffices :
  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)
⊢ Eq (α := ⨂[R] (i : ι), A i)
    ((((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
              ((((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) x :
                    (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
                  (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
                y) :
            (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        z :
      ⨂[R] (i : ι), A i)
    ((((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) x :
            (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        ((((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) y :
              (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
            (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
          z) :
      ⨂[R] (i : ι), A i)

Tactic:
suffices LinearMap.llcomp R _ _ _ mul ∘ₗ mul =
      (LinearMap.llcomp R _ _ _ LinearMap.lflip.toLinearMap <|
        LinearMap.llcomp R _ _ _ mul.flip ∘ₗ mul).flip by
    exact DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this x) y) z