-- 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 : 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
⊢ Eq (α := M ⊗[R] Q ⊗[S] P →ₗ[B] M ⊗[R] Q ⊗[S] P)
    ((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) ∘ₗ
        (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) :
      M ⊗[R] Q ⊗[S] P →ₗ[B] M ⊗[R] Q ⊗[S] P)
    (LinearMap.id : M ⊗[R] Q ⊗[S] P →ₗ[B] M ⊗[R] Q ⊗[S] P)
have a : ∀ (x : M) (x_1 : Q) (x_2 : P),
  Eq (α := M ⊗[R] Q ⊗[S] P)
    (((((((curry
                          (curry
                            ((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) ∘ₗ
                              (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))) :
                        M →ₗ[B] Q →ₗ[R] P →ₗ[S] M ⊗[R] Q ⊗[S] P) :
                      (a : M) → Q →ₗ[R] P →ₗ[S] M ⊗[R] Q ⊗[S] P)
                    x :
                  Q →ₗ[R] P →ₗ[S] M ⊗[R] Q ⊗[S] P) :
                (a : Q) → P →ₗ[S] M ⊗[R] Q ⊗[S] P)
              x_1 :
            P →ₗ[S] M ⊗[R] Q ⊗[S] P) :
          (a : P) → M ⊗[R] Q ⊗[S] P)
        x_2 :
      M ⊗[R] Q ⊗[S] P)
    (((((((curry (curry LinearMap.id) : M →ₗ[B] Q →ₗ[R] P →ₗ[S] M ⊗[R] Q ⊗[S] P) :
                      (a : M) → Q →ₗ[R] P →ₗ[S] M ⊗[R] Q ⊗[S] P)
                    x :
                  Q →ₗ[R] P →ₗ[S] M ⊗[R] Q ⊗[S] P) :
                (a : Q) → P →ₗ[S] M ⊗[R] Q ⊗[S] P)
              x_1 :
            P →ₗ[S] M ⊗[R] Q ⊗[S] P) :
          (a : P) → M ⊗[R] Q ⊗[S] P)
        x_2 :
      M ⊗[R] Q ⊗[S] P)
Tactic: ext