-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
r : R
f : M →ₗ[A] P
g : N →ₗ[R] Q
x : M
x_1 : N
a :
  Eq (α := P ⊗[R] Q)
    ((((TensorProduct.curry
                  ((↑R :
                      {S : Type uA} →
                        {M : Type (max uM uN)} →
                          {M₂ : Type (max uP uQ)} →
                            [inst : Semiring R] →
                              [inst_15 : Semiring S] →
                                [inst_16 : AddCommMonoid M] →
                                  [inst_17 : AddCommMonoid M₂] →
                                    [inst_18 : Module R M] →
                                      [inst_19 : Module R M₂] →
                                        [inst_20 : Module S M] →
                                          [inst_21 : Module S M₂] →
                                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    (map f (r • g) : M ⊗[R] N →ₗ[A] P ⊗[R] Q)) :
                (a : M) → N →ₗ[R] P ⊗[R] Q)
              x :
            N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        x_1 :
      P ⊗[R] Q)
    ((((TensorProduct.curry
                  ((↑R :
                      {S : Type uA} →
                        {M : Type (max uM uN)} →
                          {M₂ : Type (max uP uQ)} →
                            [inst : Semiring R] →
                              [inst_15 : Semiring S] →
                                [inst_16 : AddCommMonoid M] →
                                  [inst_17 : AddCommMonoid M₂] →
                                    [inst_18 : Module R M] →
                                      [inst_19 : Module R M₂] →
                                        [inst_20 : Module S M] →
                                          [inst_21 : Module S M₂] →
                                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    (HSMul.hSMul (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q) r (map f g : M ⊗[R] N →ₗ[A] P ⊗[R] Q))) :
                (a : M) → N →ₗ[R] P ⊗[R] Q)
              x :
            N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        x_1 :
      P ⊗[R] Q)
a₁ :
  Eq (α := P ⊗[R] Q)
    (((↑R :
              {S : Type uA} →
                {M : Type (max uM uN)} →
                  {M₂ : Type (max uP uQ)} →
                    [inst : Semiring R] →
                      [inst_15 : Semiring S] →
                        [inst_16 : AddCommMonoid M] →
                          [inst_17 : AddCommMonoid M₂] →
                            [inst_18 : Module R M] →
                              [inst_19 : Module R M₂] →
                                [inst_20 : Module S M] →
                                  [inst_21 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (map f (r • g) : M ⊗[R] N →ₗ[A] P ⊗[R] Q) :
          (a : M ⊗[R] N) → P ⊗[R] Q)
        (x ⊗ₜ[R] x_1) :
      P ⊗[R] Q)
    (((↑R :
              {S : Type uA} →
                {M : Type (max uM uN)} →
                  {M₂ : Type (max uP uQ)} →
                    [inst : Semiring R] →
                      [inst_15 : Semiring S] →
                        [inst_16 : AddCommMonoid M] →
                          [inst_17 : AddCommMonoid M₂] →
                            [inst_18 : Module R M] →
                              [inst_19 : Module R M₂] →
                                [inst_20 : Module S M] →
                                  [inst_21 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (HSMul.hSMul (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q) r (map f g : M ⊗[R] N →ₗ[A] P ⊗[R] Q)) :
          (a : M ⊗[R] N) → P ⊗[R] Q)
        (x ⊗ₜ[R] x_1) :
      P ⊗[R] Q)
a₂ :
  Eq (α := P ⊗[R] Q) (((map f (r • g) : M ⊗[R] N →ₗ[A] P ⊗[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) (x ⊗ₜ[R] x_1) : P ⊗[R] Q)
    ((HSMul.hSMul (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q) r (map f g : M ⊗[R] N →ₗ[A] P ⊗[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q)
        (x ⊗ₜ[R] x_1) :
      P ⊗[R] Q)
a₃ :
  ((map f (r • g) : M ⊗[R] N →ₗ[A] P ⊗[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) (x ⊗ₜ[R] x_1) =
    HSMul.hSMul (β := P ⊗[R] Q) r
      (((map f g : M ⊗[R] N →ₗ[A] P ⊗[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) (x ⊗ₜ[R] x_1) : P ⊗[R] Q)
a₄ :
  (f : (a : M) → P) x ⊗ₜ[R] (r • g : (a : N) → Q) x_1 =
    HSMul.hSMul (β := P ⊗[R] Q) r ((f : (a : M) → P) x ⊗ₜ[R] (g : (a : N) → Q) x_1 : P ⊗[R] Q)
⊢ Eq (α := P ⊗[R] Q)
    (((((curry (map f (r • g)) : M →ₗ[A] N →ₗ[R] P ⊗[R] Q) : (a : M) → N →ₗ[R] P ⊗[R] Q) x : N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        x_1 :
      P ⊗[R] Q)
    (((((curry (HSMul.hSMul (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q) r (map f g : M ⊗[R] N →ₗ[A] P ⊗[R] Q)) :
                  M →ₗ[A] N →ₗ[R] P ⊗[R] Q) :
                (a : M) → N →ₗ[R] P ⊗[R] Q)
              x :
            N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        x_1 :
      P ⊗[R] Q)
have a₅ : (f : (a : M) → P) x ⊗ₜ[R] HSMul.hSMul (β := Q) r ((g : (a : N) → Q) x_1 : Q) =
  HSMul.hSMul (β := P ⊗[R] Q) r ((f : (a : M) → P) x ⊗ₜ[R] (g : (a : N) → Q) x_1 : P ⊗[R] Q)
Tactic: simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, smul_apply, map_tmul,
    smul_apply, tmul_smul]