-- 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 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
⊢ 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)))
have 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))
Tactic: ext