-- 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 T A
inst_24 : IsScalarTower R T A
inst_25 : SMulCommClass S T A
inst_26 : Algebra S T
inst_27 : IsScalarTower S T A
inst_28 : CommSemiring R'
inst_29 : Algebra R R'
inst_30 : Algebra R' T
inst_31 : Algebra R' A
inst_32 : Algebra R' B
inst_33 : IsScalarTower R R' A
inst_34 : SMulCommClass S R' A
inst_35 : SMulCommClass R' S A
inst_36 : IsScalarTower R' T A
inst_37 : IsScalarTower R R' B
a :
  ∀ (x : A) (x_1 : B) (x_2 : C) (x_3 : D) (x_4 : A) (x_5 : B) (x_6 : C) (x_7 : D),
    Eq (α := A ⊗[S] C ⊗[R'] (B ⊗[R] D))
      (((((AlgebraTensorModule.curry
                      (((((AlgebraTensorModule.curry
                                    (AlgebraTensorModule.curry
                                      (((((AlgebraTensorModule.curry
                                                    (((((AlgebraTensorModule.curry
                                                                  (AlgebraTensorModule.curry
                                                                    (LinearMap.compr₂
                                                                      (LinearMap.mul T (A ⊗[R'] B ⊗[S] (C ⊗[R] D)))
                                                                      (↑(AlgebraTensorModule.tensorTensorTensorComm R R'
                                                                            S T A B C D) :
                                                                        A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T]
                                                                          A ⊗[S] C ⊗[R'] (B ⊗[R] D)))) :
                                                                A →ₗ[T]
                                                                  B →ₗ[R']
                                                                    C ⊗[R] D →ₗ[S]
                                                                      A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T]
                                                                        A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
                                                              (a : A) →
                                                                B →ₗ[R']
                                                                  C ⊗[R] D →ₗ[S]
                                                                    A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T]
                                                                      A ⊗[S] C ⊗[R'] (B ⊗[R] D))
                                                            x :
                                                          B →ₗ[R']
                                                            C ⊗[R] D →ₗ[S]
                                                              A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T]
                                                                A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
                                                        (a : B) →
                                                          C ⊗[R] D →ₗ[S]
                                                            A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D))
                                                      x_1) :
                                                  C →ₗ[S]
                                                    D →ₗ[R] A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
                                                (a : C) →
                                                  D →ₗ[R] A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D))
                                              x_2 :
                                            D →ₗ[R] A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
                                          (a : D) → A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D))
                                        x_3)) :
                                  A →ₗ[T] B →ₗ[R'] C ⊗[R] D →ₗ[S] A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
                                (a : A) → B →ₗ[R'] C ⊗[R] D →ₗ[S] A ⊗[S] C ⊗[R'] (B ⊗[R] D))
                              x_4 :
                            B →ₗ[R'] C ⊗[R] D →ₗ[S] A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
                          (a : B) → C ⊗[R] D →ₗ[S] A ⊗[S] C ⊗[R'] (B ⊗[R] D))
                        x_5) :
                    C →ₗ[S] D →ₗ[R] A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
                  (a : C) → D →ₗ[R] A ⊗[S] C ⊗[R'] (B ⊗[R] D))
                x_6 :
              D →ₗ[R] A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
            (a : D) → A ⊗[S] C ⊗[R'] (B ⊗[R] D))
          x_7 :
        A ⊗[S] C ⊗[R'] (B ⊗[R] D))
      (((((AlgebraTensorModule.curry
                      (((((AlgebraTensorModule.curry
                                    (AlgebraTensorModule.curry
                                      (((((AlgebraTensorModule.curry
                                                    (((((AlgebraTensorModule.curry
                                                                  (AlgebraTensorModule.curry
                                                                    (LinearMap.compl₂
                                                                      (LinearMap.mul T (A ⊗[S] C ⊗[R'] (B ⊗[R] D)) ∘ₗ
                                                                        (↑(AlgebraTensorModule.tensorTensorTensorComm R
                                                                              R' S T A B C D) :
                                                                          A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T]
                                                                            A ⊗[S] C ⊗[R'] (B ⊗[R] D)))
                                                                      (↑(AlgebraTensorModule.tensorTensorTensorComm R R'
                                                                            S T A B C D) :
                                                                        A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T]
                                                                          A ⊗[S] C ⊗[R'] (B ⊗[R] D)))) :
                                                                A →ₗ[T]
                                                                  B →ₗ[R']
                                                                    C ⊗[R] D →ₗ[S]
                                                                      A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T]
                                                                        A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
                                                              (a : A) →
                                                                B →ₗ[R']
                                                                  C ⊗[R] D →ₗ[S]
                                                                    A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T]
                                                                      A ⊗[S] C ⊗[R'] (B ⊗[R] D))
                                                            x :
                                                          B →ₗ[R']
                                                            C ⊗[R] D →ₗ[S]
                                                              A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T]
                                                                A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
                                                        (a : B) →
                                                          C ⊗[R] D →ₗ[S]
                                                            A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D))
                                                      x_1) :
                                                  C →ₗ[S]
                                                    D →ₗ[R] A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
                                                (a : C) →
                                                  D →ₗ[R] A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D))
                                              x_2 :
                                            D →ₗ[R] A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
                                          (a : D) → A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D))
                                        x_3)) :
                                  A →ₗ[T] B →ₗ[R'] C ⊗[R] D →ₗ[S] A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
                                (a : A) → B →ₗ[R'] C ⊗[R] D →ₗ[S] A ⊗[S] C ⊗[R'] (B ⊗[R] D))
                              x_4 :
                            B →ₗ[R'] C ⊗[R] D →ₗ[S] A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
                          (a : B) → C ⊗[R] D →ₗ[S] A ⊗[S] C ⊗[R'] (B ⊗[R] D))
                        x_5) :
                    C →ₗ[S] D →ₗ[R] A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
                  (a : C) → D →ₗ[R] A ⊗[S] C ⊗[R'] (B ⊗[R] D))
                x_6 :
              D →ₗ[R] A ⊗[S] C ⊗[R'] (B ⊗[R] D)) :
            (a : D) → A ⊗[S] C ⊗[R'] (B ⊗[R] D))
          x_7 :
        A ⊗[S] C ⊗[R'] (B ⊗[R] D))
⊢ Eq (α := A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T] A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D))
    (LinearMap.compr₂ (LinearMap.mul T (A ⊗[R'] B ⊗[S] (C ⊗[R] D)))
      (↑(AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D) :
        A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D)))
    (LinearMap.compl₂
      (LinearMap.mul T (A ⊗[S] C ⊗[R'] (B ⊗[R] D)) ∘ₗ
        (↑(AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D) :
          A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D)))
      (↑(AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D) :
        A ⊗[R'] B ⊗[S] (C ⊗[R] D) →ₗ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D)))

Tactic:
ext