-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
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
⊢ 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)))
have 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))
Tactic: ext