-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
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
⊢ Eq (α := 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)) ∘ₗ
        (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) :
      M ⊗[A] (P ⊗[R] Q) →ₗ[B] M ⊗[A] (P ⊗[R] Q))
    (LinearMap.id : M ⊗[A] (P ⊗[R] Q) →ₗ[B] M ⊗[A] (P ⊗[R] Q))
have a : ∀ (x : M) (x_1 : P) (x_2 : Q),
  Eq (α := M ⊗[A] (P ⊗[R] Q))
    (((((curry
                    (((curry
                            ((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)) ∘ₗ
                              (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)) :
                          M →ₗ[B] P ⊗[R] Q →ₗ[A] M ⊗[A] (P ⊗[R] Q)) :
                        (a : M) → P ⊗[R] Q →ₗ[A] 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 ⊗[R] Q →ₗ[A] M ⊗[A] (P ⊗[R] Q)) :
                        (a : M) → P ⊗[R] Q →ₗ[A] 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))
Tactic: ext