-- 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
a :
  ∀ (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)
⊢ Eq (α := 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)
          mul ∘ₗ
        mul :
      A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
    (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)

Tactic:
ext xa xb ya yb za zb