-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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
⊢ 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)
have 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)
Tactic: ext xa xb ya yb za zb