-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : Module B M
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
inst_12 : AddCommMonoid N
inst_13 : Module R N
inst_14 : AddCommMonoid P
inst_15 : Module A P
inst_16 : AddCommMonoid P'
inst_17 : Module A P'
inst_18 : AddCommMonoid Q
inst_19 : Module R Q
inst_20 : CommSemiring S
inst_21 : Module S M
inst_22 : Module S P
inst_23 : Algebra S B
inst_24 : IsScalarTower S B M
inst_25 : SMulCommClass R S M
inst_26 : SMulCommClass S R M
a :
  ∀ (x : M) (x_1 : P) (x_2 : Q),
    Eq (α := M ⊗[S] P ⊗[R] Q)
      (((((((curry
                            (curry
                              ((lift
                                    (lift
                                      ((↑lflip :
                                            (P →ₗ[S] Q →ₗ[R] M ⊗[S] P ⊗[R] Q) →ₗ[B] Q →ₗ[R] P →ₗ[S] M ⊗[S] P ⊗[R] Q) ∘ₗ
                                          compr₂ (mk S B M P) (mk R B (M ⊗[S] P) Q) :
                                        M →ₗ[B] Q →ₗ[R] P →ₗ[S] M ⊗[S] P ⊗[R] Q)) :
                                  M ⊗[R] Q ⊗[S] P →ₗ[B] M ⊗[S] P ⊗[R] Q) ∘ₗ
                                (lift
                                    (lift
                                      ((↑lflip :
                                            (Q →ₗ[R] P →ₗ[S] M ⊗[R] Q ⊗[S] P) →ₗ[B] P →ₗ[S] Q →ₗ[R] M ⊗[R] Q ⊗[S] P) ∘ₗ
                                          compr₂ (mk R B M Q) (mk S B (M ⊗[R] Q) P) :
                                        M →ₗ[B] P →ₗ[S] Q →ₗ[R] M ⊗[R] Q ⊗[S] P)) :
                                  M ⊗[S] P ⊗[R] Q →ₗ[B] M ⊗[R] Q ⊗[S] P))) :
                          M →ₗ[B] P →ₗ[S] Q →ₗ[R] M ⊗[S] P ⊗[R] Q) :
                        (a : M) → P →ₗ[S] Q →ₗ[R] M ⊗[S] P ⊗[R] Q)
                      x :
                    P →ₗ[S] Q →ₗ[R] M ⊗[S] P ⊗[R] Q) :
                  (a : P) → Q →ₗ[R] M ⊗[S] P ⊗[R] Q)
                x_1 :
              Q →ₗ[R] M ⊗[S] P ⊗[R] Q) :
            (a : Q) → M ⊗[S] P ⊗[R] Q)
          x_2 :
        M ⊗[S] P ⊗[R] Q)
      (((((((curry (curry LinearMap.id) : M →ₗ[B] P →ₗ[S] Q →ₗ[R] M ⊗[S] P ⊗[R] Q) :
                        (a : M) → P →ₗ[S] Q →ₗ[R] M ⊗[S] P ⊗[R] Q)
                      x :
                    P →ₗ[S] Q →ₗ[R] M ⊗[S] P ⊗[R] Q) :
                  (a : P) → Q →ₗ[R] M ⊗[S] P ⊗[R] Q)
                x_1 :
              Q →ₗ[R] M ⊗[S] P ⊗[R] Q) :
            (a : Q) → M ⊗[S] P ⊗[R] Q)
          x_2 :
        M ⊗[S] P ⊗[R] Q)
⊢ Eq (α := M ⊗[S] P ⊗[R] Q →ₗ[B] M ⊗[S] P ⊗[R] Q)
    ((lift
            (lift
              ((↑lflip : (P →ₗ[S] Q →ₗ[R] M ⊗[S] P ⊗[R] Q) →ₗ[B] Q →ₗ[R] P →ₗ[S] M ⊗[S] P ⊗[R] Q) ∘ₗ
                  compr₂ (mk S B M P) (mk R B (M ⊗[S] P) Q) :
                M →ₗ[B] Q →ₗ[R] P →ₗ[S] M ⊗[S] P ⊗[R] Q)) :
          M ⊗[R] Q ⊗[S] P →ₗ[B] M ⊗[S] P ⊗[R] Q) ∘ₗ
        (lift
            (lift
              ((↑lflip : (Q →ₗ[R] P →ₗ[S] M ⊗[R] Q ⊗[S] P) →ₗ[B] P →ₗ[S] Q →ₗ[R] M ⊗[R] Q ⊗[S] P) ∘ₗ
                  compr₂ (mk R B M Q) (mk S B (M ⊗[R] Q) P) :
                M →ₗ[B] P →ₗ[S] Q →ₗ[R] M ⊗[R] Q ⊗[S] P)) :
          M ⊗[S] P ⊗[R] Q →ₗ[B] M ⊗[R] Q ⊗[S] P) :
      M ⊗[S] P ⊗[R] Q →ₗ[B] M ⊗[S] P ⊗[R] Q)
    (LinearMap.id : M ⊗[S] P ⊗[R] Q →ₗ[B] M ⊗[S] P ⊗[R] Q)

Tactic:
ext