-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : Semiring D
inst_14 : Algebra R D
inst_15 : Semiring E
inst_16 : Algebra R E
inst_17 : Algebra S E
inst_18 : IsScalarTower R S E
inst_19 : Semiring F
inst_20 : Algebra R F
inst_21 : CommSemiring T
inst_22 : Algebra R T
inst_23 : Algebra S T
inst_24 : Algebra T A
inst_25 : IsScalarTower R T A
inst_26 : IsScalarTower S T A
a :
  ∀ (x : A) (x_1 : C) (x_2 : D) (x_3 : A) (x_4 : C) (x_5 : D),
    Eq (α := A ⊗[S] (C ⊗[R] D))
      (((((((AlgebraTensorModule.curry
                            (AlgebraTensorModule.curry
                              (((((((AlgebraTensorModule.curry
                                                  (AlgebraTensorModule.curry
                                                    (LinearMap.compr₂ (LinearMap.mul T (A ⊗[S] C ⊗[R] D))
                                                      (↑(AlgebraTensorModule.assoc R S T A C D) :
                                                        A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D)))) :
                                                A →ₗ[T] C →ₗ[S] D →ₗ[R] A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D)) :
                                              (a : A) → C →ₗ[S] D →ₗ[R] A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D))
                                            x :
                                          C →ₗ[S] D →ₗ[R] A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D)) :
                                        (a : C) → D →ₗ[R] A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D))
                                      x_1 :
                                    D →ₗ[R] A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D)) :
                                  (a : D) → A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D))
                                x_2)) :
                          A →ₗ[T] C →ₗ[S] D →ₗ[R] A ⊗[S] (C ⊗[R] D)) :
                        (a : A) → C →ₗ[S] D →ₗ[R] A ⊗[S] (C ⊗[R] D))
                      x_3 :
                    C →ₗ[S] D →ₗ[R] A ⊗[S] (C ⊗[R] D)) :
                  (a : C) → D →ₗ[R] A ⊗[S] (C ⊗[R] D))
                x_4 :
              D →ₗ[R] A ⊗[S] (C ⊗[R] D)) :
            (a : D) → A ⊗[S] (C ⊗[R] D))
          x_5 :
        A ⊗[S] (C ⊗[R] D))
      (((((((AlgebraTensorModule.curry
                            (AlgebraTensorModule.curry
                              (((((((AlgebraTensorModule.curry
                                                  (AlgebraTensorModule.curry
                                                    (LinearMap.compl₂
                                                      (LinearMap.mul T (A ⊗[S] (C ⊗[R] D)) ∘ₗ
                                                        (↑(AlgebraTensorModule.assoc R S T A C D) :
                                                          A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D)))
                                                      (↑(AlgebraTensorModule.assoc R S T A C D) :
                                                        A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D)))) :
                                                A →ₗ[T] C →ₗ[S] D →ₗ[R] A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D)) :
                                              (a : A) → C →ₗ[S] D →ₗ[R] A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D))
                                            x :
                                          C →ₗ[S] D →ₗ[R] A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D)) :
                                        (a : C) → D →ₗ[R] A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D))
                                      x_1 :
                                    D →ₗ[R] A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D)) :
                                  (a : D) → A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D))
                                x_2)) :
                          A →ₗ[T] C →ₗ[S] D →ₗ[R] A ⊗[S] (C ⊗[R] D)) :
                        (a : A) → C →ₗ[S] D →ₗ[R] A ⊗[S] (C ⊗[R] D))
                      x_3 :
                    C →ₗ[S] D →ₗ[R] A ⊗[S] (C ⊗[R] D)) :
                  (a : C) → D →ₗ[R] A ⊗[S] (C ⊗[R] D))
                x_4 :
              D →ₗ[R] A ⊗[S] (C ⊗[R] D)) :
            (a : D) → A ⊗[S] (C ⊗[R] D))
          x_5 :
        A ⊗[S] (C ⊗[R] D))
⊢ Eq (α := A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D))
    (LinearMap.compr₂ (LinearMap.mul T (A ⊗[S] C ⊗[R] D))
      (↑(AlgebraTensorModule.assoc R S T A C D) : A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D)))
    (LinearMap.compl₂
      (LinearMap.mul T (A ⊗[S] (C ⊗[R] D)) ∘ₗ
        (↑(AlgebraTensorModule.assoc R S T A C D) : A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D)))
      (↑(AlgebraTensorModule.assoc R S T A C D) : A ⊗[S] C ⊗[R] D →ₗ[T] A ⊗[S] (C ⊗[R] D)))

Tactic:
ext