-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
x y z : A ⊗[R] B
xa : A
xb : B
ya : A
yb : B
za : A
zb : B
⊢ Eq (α := A ⊗[R] B)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (((((AlgebraTensorModule.curry
                                                ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                                                      (a : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
                                                        (A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R]
                                                          A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                                                    mul ∘ₗ
                                                  mul) :
                                              A →ₗ[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                                            (a : A) → B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                                          xa :
                                        B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                                      (a : B) → A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                                    xb) :
                                A →ₗ[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                              (a : A) → B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                            ya :
                          B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                        (a : B) → A ⊗[R] B →ₗ[R] A ⊗[R] B)
                      yb) :
                  A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : A) → B →ₗ[R] A ⊗[R] B)
              za :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        zb :
      A ⊗[R] B)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (((((AlgebraTensorModule.curry
                                                (LinearMap.flip
                                                  ((((LinearMap.llcomp R (A ⊗[R] B)
                                                              (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                                                              (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                                                            (a :
                                                                (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R]
                                                                  A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
                                                              (A ⊗[R] B →ₗ[R]
                                                                  A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R]
                                                                A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                                                          (↑LinearMap.lflip :
                                                            (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R]
                                                              A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                                                        (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R]
                                                          A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                                                      (a : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
                                                        A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                                                    ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B)
                                                            (A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                                                          (a : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) →
                                                            (A ⊗[R] B →ₗ[R] A ⊗[R] B) →ₗ[R]
                                                              A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                                                        (LinearMap.flip mul) ∘ₗ
                                                      mul))) :
                                              A →ₗ[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                                            (a : A) → B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                                          xa :
                                        B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                                      (a : B) → A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                                    xb) :
                                A →ₗ[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                              (a : A) → B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                            ya :
                          B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) :
                        (a : B) → A ⊗[R] B →ₗ[R] A ⊗[R] B)
                      yb) :
                  A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : A) → B →ₗ[R] A ⊗[R] B)
              za :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        zb :
      A ⊗[R] B)

Tactic:
congr_arg₂ (· ⊗ₜ ·) (mul_assoc xa ya za) (mul_assoc xb yb zb)

Premises used: Quotient.liftOn', AddCon.liftOn, mul_assoc, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, congr_arg₂