Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: 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✝³⁶ : CommSemiring S
inst✝³⁵ : Algebra R S
inst✝³⁴ : Semiring A
inst✝³³ : Algebra R A
inst✝³² : Algebra S A
inst✝³¹ : IsScalarTower R S A
inst✝³⁰ : Semiring B
inst✝²⁹ : Algebra R B
inst✝²⁸ : Semiring C
inst✝²⁷ : Algebra R C
inst✝²⁶ : Algebra S C
inst✝²⁵ : IsScalarTower R S C
inst✝²⁴ : Semiring D
inst✝²³ : Algebra R D
inst✝²² : Semiring E
inst✝²¹ : Algebra R E
inst✝²⁰ : Algebra S E
inst✝¹⁹ : IsScalarTower R S E
inst✝¹⁸ : Semiring F
inst✝¹⁷ : Algebra R F
inst✝¹⁶ : CommSemiring T
inst✝¹⁵ : Algebra R T
inst✝¹⁴ : Algebra T A
inst✝¹³ : IsScalarTower R T A
inst✝¹² : SMulCommClass S T A
inst✝¹¹ : Algebra S T
inst✝¹⁰ : IsScalarTower S T A
inst✝⁹ : CommSemiring R'
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra R' T
inst✝⁶ : Algebra R' A
inst✝⁵ : Algebra R' B
inst✝⁴ : IsScalarTower R R' A
inst✝³ : SMulCommClass S R' A
inst✝² : SMulCommClass R' S A
inst✝¹ : IsScalarTower R' T A
inst✝ : IsScalarTower R R' B
⊢ (LinearMap.mul T (A ⊗[R'] B ⊗[S] (C ⊗[R] D))).compr₂ ↑(AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D) =
    (LinearMap.mul T (A ⊗[S] C ⊗[R'] (B ⊗[R] D)) ∘ₗ
          ↑(AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D)).compl₂
      ↑(AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D)

Tactic:
ext

Goal state after:
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✝³⁶ : CommSemiring S
inst✝³⁵ : Algebra R S
inst✝³⁴ : Semiring A
inst✝³³ : Algebra R A
inst✝³² : Algebra S A
inst✝³¹ : IsScalarTower R S A
inst✝³⁰ : Semiring B
inst✝²⁹ : Algebra R B
inst✝²⁸ : Semiring C
inst✝²⁷ : Algebra R C
inst✝²⁶ : Algebra S C
inst✝²⁵ : IsScalarTower R S C
inst✝²⁴ : Semiring D
inst✝²³ : Algebra R D
inst✝²² : Semiring E
inst✝²¹ : Algebra R E
inst✝²⁰ : Algebra S E
inst✝¹⁹ : IsScalarTower R S E
inst✝¹⁸ : Semiring F
inst✝¹⁷ : Algebra R F
inst✝¹⁶ : CommSemiring T
inst✝¹⁵ : Algebra R T
inst✝¹⁴ : Algebra T A
inst✝¹³ : IsScalarTower R T A
inst✝¹² : SMulCommClass S T A
inst✝¹¹ : Algebra S T
inst✝¹⁰ : IsScalarTower S T A
inst✝⁹ : CommSemiring R'
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra R' T
inst✝⁶ : Algebra R' A
inst✝⁵ : Algebra R' B
inst✝⁴ : IsScalarTower R R' A
inst✝³ : SMulCommClass S R' A
inst✝² : SMulCommClass R' S A
inst✝¹ : IsScalarTower R' T A
inst✝ : IsScalarTower R R' B
x✝⁷ : A
x✝⁶ : B
x✝⁵ : C
x✝⁴ : D
x✝³ : A
x✝² : B
x✝¹ : C
x✝ : D
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry
                        (((AlgebraTensorModule.curry
                              (AlgebraTensorModule.curry
                                ((LinearMap.mul T (A ⊗[R'] B ⊗[S] (C ⊗[R] D))).compr₂
                                  ↑(AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D))))
                            x✝⁷)
                          x✝⁶))
                      x✝⁵)
                    x✝⁴)))
              x✝³)
            x✝²))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry
                        (((AlgebraTensorModule.curry
                              (AlgebraTensorModule.curry
                                ((LinearMap.mul T (A ⊗[S] C ⊗[R'] (B ⊗[R] D)) ∘ₗ
                                      ↑(AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D)).compl₂
                                  ↑(AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D))))
                            x✝⁷)
                          x✝⁶))
                      x✝⁵)
                    x✝⁴)))
              x✝³)
            x✝²))
        x✝¹)
      x✝