-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring 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 : IsScalarTower R A M
inst_9 : AddCommMonoid N
inst_10 : Module R N
inst_11 : AddCommMonoid P
inst_12 : Module R P
inst_13 : Module A P
inst_14 : IsScalarTower R A P
inst_15 : AddCommMonoid Q
inst_16 : Module R Q
inst_17 : Module B P
inst_18 : IsScalarTower R B P
inst_19 : SMulCommClass A B P
b : B
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_20 : Semiring S] →
                                [inst_21 : AddCommMonoid M] →
                                  [inst_22 : AddCommMonoid M₂] →
                                    [inst_23 : Module R M] →
                                      [inst_24 : Module R M₂] →
                                        [inst_25 : Module S M] →
                                          [inst_26 : Module S M₂] →
                                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    (map (b • 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)
    ((((TensorProduct.curry
                  ((↑R :
                      {S : Type uA} →
                        {M : Type (max uM uN)} →
                          {M₂ : Type (max uP uQ)} →
                            [inst : Semiring R] →
                              [inst_20 : Semiring S] →
                                [inst_21 : AddCommMonoid M] →
                                  [inst_22 : AddCommMonoid M₂] →
                                    [inst_23 : Module R M] →
                                      [inst_24 : Module R M₂] →
                                        [inst_25 : Module S M] →
                                          [inst_26 : 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) b (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_20 : Semiring S] →
                        [inst_21 : AddCommMonoid M] →
                          [inst_22 : AddCommMonoid M₂] →
                            [inst_23 : Module R M] →
                              [inst_24 : Module R M₂] →
                                [inst_25 : Module S M] →
                                  [inst_26 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (map (b • f) 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_20 : Semiring S] →
                        [inst_21 : AddCommMonoid M] →
                          [inst_22 : AddCommMonoid M₂] →
                            [inst_23 : Module R M] →
                              [inst_24 : Module R M₂] →
                                [inst_25 : Module S M] →
                                  [inst_26 : 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) b (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 (b • f) 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) b (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 (b • f) g : M ⊗[R] N →ₗ[A] P ⊗[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) (x ⊗ₜ[R] x_1) =
    HSMul.hSMul (β := P ⊗[R] Q) b
      (((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₄ :
  (b • f : (a : M) → P) x ⊗ₜ[R] (g : (a : N) → Q) x_1 =
    HSMul.hSMul (β := P ⊗[R] Q) b ((f : (a : M) → P) x ⊗ₜ[R] (g : (a : N) → Q) x_1 : P ⊗[R] Q)
⊢ Eq (α := P ⊗[R] Q)
    (((((curry (map (b • f) 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) b (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₅ : HSMul.hSMul (β := P) b ((f : (a : M) → P) x : P) ⊗ₜ[R] (g : (a : N) → Q) x_1 =
  HSMul.hSMul (β := P ⊗[R] Q) b ((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, smul_tmul']