-- 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 : Module R P
inst_21 : IsScalarTower R A P
inst_22 : Algebra A B
inst_23 : IsScalarTower A B M
a :
  ∀ (x : M) (x_1 : P) (x_2 : Q),
    Eq (α := M ⊗[A] P ⊗[R] Q)
      (((((((curry
                            (curry
                              ((lift
                                    ((uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) :
                                        (P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q) →ₗ[B] P ⊗[R] Q →ₗ[A] M ⊗[A] P ⊗[R] Q) ∘ₗ
                                      (curry (mk R B (M ⊗[A] P) Q) : M →ₗ[B] P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q)) :
                                  M ⊗[A] (P ⊗[R] Q) →ₗ[B] M ⊗[A] P ⊗[R] Q) ∘ₗ
                                (lift
                                    (lift
                                      ((lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) :
                                            (P ⊗[R] Q →ₗ[A] M ⊗[A] (P ⊗[R] Q)) →ₗ[B]
                                              P →ₗ[A] Q →ₗ[R] M ⊗[A] (P ⊗[R] Q)) ∘ₗ
                                          (mk A B M (P ⊗[R] Q) : M →ₗ[B] P ⊗[R] Q →ₗ[A] M ⊗[A] (P ⊗[R] Q)) :
                                        M →ₗ[B] P →ₗ[A] Q →ₗ[R] M ⊗[A] (P ⊗[R] Q))) :
                                  M ⊗[A] P ⊗[R] Q →ₗ[B] M ⊗[A] (P ⊗[R] Q)))) :
                          M →ₗ[B] P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q) :
                        (a : M) → P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q)
                      x :
                    P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q) :
                  (a : P) → Q →ₗ[R] M ⊗[A] P ⊗[R] Q)
                x_1 :
              Q →ₗ[R] M ⊗[A] P ⊗[R] Q) :
            (a : Q) → M ⊗[A] P ⊗[R] Q)
          x_2 :
        M ⊗[A] P ⊗[R] Q)
      (((((((curry (curry LinearMap.id) : M →ₗ[B] P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q) :
                        (a : M) → P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q)
                      x :
                    P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q) :
                  (a : P) → Q →ₗ[R] M ⊗[A] P ⊗[R] Q)
                x_1 :
              Q →ₗ[R] M ⊗[A] P ⊗[R] Q) :
            (a : Q) → M ⊗[A] P ⊗[R] Q)
          x_2 :
        M ⊗[A] P ⊗[R] Q)
⊢ Eq (α := M ⊗[A] P ⊗[R] Q →ₗ[B] M ⊗[A] P ⊗[R] Q)
    ((lift
            ((uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) :
                (P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q) →ₗ[B] P ⊗[R] Q →ₗ[A] M ⊗[A] P ⊗[R] Q) ∘ₗ
              (curry (mk R B (M ⊗[A] P) Q) : M →ₗ[B] P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q)) :
          M ⊗[A] (P ⊗[R] Q) →ₗ[B] M ⊗[A] P ⊗[R] Q) ∘ₗ
        (lift
            (lift
              ((lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) :
                    (P ⊗[R] Q →ₗ[A] M ⊗[A] (P ⊗[R] Q)) →ₗ[B] P →ₗ[A] Q →ₗ[R] M ⊗[A] (P ⊗[R] Q)) ∘ₗ
                  (mk A B M (P ⊗[R] Q) : M →ₗ[B] P ⊗[R] Q →ₗ[A] M ⊗[A] (P ⊗[R] Q)) :
                M →ₗ[B] P →ₗ[A] Q →ₗ[R] M ⊗[A] (P ⊗[R] Q))) :
          M ⊗[A] P ⊗[R] Q →ₗ[B] M ⊗[A] (P ⊗[R] Q)) :
      M ⊗[A] P ⊗[R] Q →ₗ[B] M ⊗[A] P ⊗[R] Q)
    (LinearMap.id : M ⊗[A] P ⊗[R] Q →ₗ[B] M ⊗[A] P ⊗[R] Q)

Tactic:
ext