-- 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)
    ((((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)
have 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)
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